26 fun ml_val vs stru txt = |
26 fun ml_val vs stru txt = |
27 txt |> ml_with_struct stru |
27 txt |> ml_with_struct stru |
28 |> ml_with_vars vs |
28 |> ml_with_vars vs |
29 |
29 |
30 fun ml_pat pat lhs = |
30 fun ml_pat pat lhs = |
31 ML_Lex.read "val " @ ML_Lex.read (translate_string (fn "\<dots>" => "_" | s => s) pat) @ |
31 ML_Lex.read "val " @ ML_Lex.read_source false pat @ |
32 ML_Lex.read " = " @ |
32 ML_Lex.read " = " @ |
33 ML_Lex.read_source false lhs |
33 ML_Lex.read_source false lhs |
|
34 |
34 |
35 |
35 fun ml_struct src = |
36 fun ml_struct src = |
36 ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ |
37 ML_Lex.read "functor DUMMY_FUNCTOR() = struct structure DUMMY = " @ |
37 ML_Lex.read_source false src @ |
38 ML_Lex.read_source false src @ |
38 ML_Lex.read " end" |
39 ML_Lex.read " end" |
87 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
88 outfn {main = Code txt, minor = Plain "type"} (split_lines txt)) |
88 |
89 |
89 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
90 fun output_type ctxt = gen_output_type (K (output ctxt)) ctxt |
90 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
91 fun output_type_ind ctxt = gen_output_type (output_indexed ctxt) ctxt |
91 |
92 |
|
93 val dots_pat = translate_string (fn "_" => "\<dots>" | s => s) |
|
94 |
92 (* checks and expression against a result pattern *) |
95 (* checks and expression against a result pattern *) |
93 fun output_response ctxt (lhs, pat) = |
96 fun output_response ctxt (lhs, pat) = |
94 (eval_fn ctxt (ml_pat pat) lhs; |
97 (eval_fn ctxt (ml_pat pat) lhs; |
95 (*eval_fn ctxt (ml_out lhs);*) (*FIXME remove*) |
98 output ctxt ((prefix_lines "" (Input.source_content lhs)) @ |
96 output ctxt ((prefix_lines "" (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
99 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
97 |
100 |
98 (* checks the expressions, but does not check it against a result pattern *) |
101 (* checks the expressions, but does not check it against a result pattern *) |
99 fun output_response_fake ctxt (lhs, pat) = |
102 fun output_response_fake ctxt (lhs, pat) = |
100 (eval_fn ctxt (ml_val [] NONE) lhs; |
103 (eval_fn ctxt (ml_val [] NONE) lhs; |
101 (*eval_fn ctxt (ml_out lhs);*) (* FIXME remove *) |
104 output ctxt ( (split_lines (Input.source_content lhs)) @ |
102 output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
105 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
103 |
106 |
104 (* checks the expressions, but does not check it against a result pattern *) |
107 (* checks the expressions, but does not check it against a result pattern *) |
105 fun ouput_response_fake_both ctxt (lhs, pat) = |
108 fun ouput_response_fake_both ctxt (lhs, pat) = |
106 (output ctxt ((split_lines (Input.source_content lhs)) @ (prefix_lines "> " pat))) |
109 (output ctxt ((split_lines (Input.source_content lhs)) @ |
|
110 (prefix_lines "> " (dots_pat (Input.source_content pat))))) |
107 |
111 |
108 val single_arg = Scan.lift (Args.name) |
112 val single_arg = Scan.lift (Args.name) |
109 val two_args = Scan.lift (Args.text_input -- Args.name) |
113 val two_args = Scan.lift (Args.text_input -- Args.text_input) |
110 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
114 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with" |-- Args.name)) |
111 |
115 |
112 val ml_setup = |
116 val ml_setup = |
113 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
117 Thy_Output.antiquotation_raw @{binding "ML"} parser_ml output_ml |
114 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |
118 #> Thy_Output.antiquotation_raw @{binding "ML_ind"} parser_ml_ind output_ml_ind |