equal
deleted
inserted
replaced
42 |
42 |
43 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt |
43 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt |
44 |
44 |
45 fun output_ml {context = ctxt, ...} code_txt = |
45 fun output_ml {context = ctxt, ...} code_txt = |
46 (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); |
46 (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); |
47 Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) |
47 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
48 |
48 |
49 val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
49 val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
50 |
50 |
51 text {* |
51 text {* |
52 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
52 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
73 can improve the code above slightly by writing |
73 can improve the code above slightly by writing |
74 *} |
74 *} |
75 |
75 |
76 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
76 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
77 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
77 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
78 Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) |
78 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
79 |
79 |
80 val _ = Thy_Output.antiquotation "ML_checked" |
80 val _ = Thy_Output.antiquotation "ML_checked" |
81 (Scan.lift (Parse.position Args.name)) output_ml *} |
81 (Scan.lift (Parse.position Args.name)) output_ml *} |
82 |
82 |
83 text {* |
83 text {* |
131 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); |
131 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); |
132 let |
132 let |
133 val code_output = space_explode "\n" code_txt |
133 val code_output = space_explode "\n" code_txt |
134 val resp_output = add_resp (space_explode "\n" pat) |
134 val resp_output = add_resp (space_explode "\n" pat) |
135 in |
135 in |
136 Thy_Output.output (map Pretty.str (code_output @ resp_output)) |
136 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
137 end) |
137 end) |
138 |
138 |
139 val _ = Thy_Output.antiquotation "ML_resp" |
139 val _ = Thy_Output.antiquotation "ML_resp" |
140 (Scan.lift (Parse.position (Args.name -- Args.name))) |
140 (Scan.lift (Parse.position (Args.name -- Args.name))) |
141 output_ml_resp*} |
141 output_ml_resp*} |