diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/antiquote_setup.ML --- 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 "\" => "_" | 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 "_" => "\" | 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 =