ProgTutorial/antiquote_setup.ML
changeset 566 6103b0eadbf2
parent 564 6e2479089226
child 567 f7c97e64cc2a
--- a/ProgTutorial/antiquote_setup.ML	Tue May 14 17:10:47 2019 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue May 14 17:45:13 2019 +0200
@@ -28,10 +28,11 @@
         |> ml_with_vars vs 
 
 fun ml_pat pat lhs =
-  ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ 
+  ML_Lex.read "val " @ ML_Lex.read_source false pat @ 
   ML_Lex.read " = " @
   ML_Lex.read_source false lhs 
 
+
 fun ml_struct src = 
   ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @
   ML_Lex.read_source false src @
@@ -89,24 +90,27 @@
 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt
 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt 
 
+val dots_pat = translate_string (fn "_" => "\<dots>"  | s => s) 
+
 (* checks and expression against a result pattern *)
 fun output_response ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_pat pat) lhs;
-     (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*)
-     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+     output ctxt ((prefix_lines "" (Input.source_content lhs)) @ 
+       (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun output_response_fake ctxt (lhs, pat) = 
     (eval_fn ctxt (ml_val [] NONE) lhs;
-     (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *)
-     output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+     output ctxt ( (split_lines (Input.source_content lhs)) @ 
+        (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 (* checks the expressions, but does not check it against a result pattern *)
 fun ouput_response_fake_both ctxt (lhs, pat) = 
-    (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat)))
+    (output ctxt ((split_lines (Input.source_content lhs)) @ 
+     (prefix_lines "> " (dots_pat (Input.source_content pat)))))
 
 val single_arg = Scan.lift (Args.name)
-val two_args   = Scan.lift (Args.text_input -- Args.name)
+val two_args   = Scan.lift (Args.text_input -- Args.text_input)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
 val ml_setup =