equal
deleted
inserted
replaced
44 |
44 |
45 fun output_ml {context = ctxt, ...} code_txt = |
45 fun output_ml {context = ctxt, ...} code_txt = |
46 let |
46 let |
47 val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none} |
47 val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none} |
48 in |
48 in |
49 (ML_Context.eval_source_in (SOME ctxt) false srcpos; |
49 (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; |
50 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
50 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
51 end |
51 end |
52 |
52 |
53 val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*} |
53 val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*} |
54 |
54 |
81 |
81 |
82 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
82 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
83 let |
83 let |
84 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
84 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
85 in |
85 in |
86 (ML_Context.eval_source_in (SOME ctxt) false srcpos; |
86 (ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos; |
87 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
87 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
88 end |
88 end |
89 |
89 |
90 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
90 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
91 (Scan.lift (Parse.position Args.name)) output_ml *} |
91 (Scan.lift (Parse.position Args.name)) output_ml *} |
141 |
141 |
142 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = |
142 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = |
143 (let |
143 (let |
144 val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} |
144 val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} |
145 in |
145 in |
146 ML_Context.eval_source_in (SOME ctxt) false srcpos |
146 ML_Context.eval_source_in (SOME ctxt) ML_Compiler.flags srcpos |
147 end; |
147 end; |
148 let |
148 let |
149 val code_output = space_explode "\n" code_txt |
149 val code_output = space_explode "\n" code_txt |
150 val resp_output = add_resp (space_explode "\n" pat) |
150 val resp_output = add_resp (space_explode "\n" pat) |
151 in |
151 in |