equal
deleted
inserted
replaced
38 document antiquotation is as follows: |
38 document antiquotation is as follows: |
39 |
39 |
40 \<close> |
40 \<close> |
41 ML \<open>Input.pos_of\<close> |
41 ML \<open>Input.pos_of\<close> |
42 ML%linenosgray\<open>fun ml_enclose bg en source = |
42 ML%linenosgray\<open>fun ml_enclose bg en source = |
43 ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\<close> |
43 ML_Lex.read bg @ ML_Lex.read_source source @ ML_Lex.read en;\<close> |
44 |
44 |
45 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
45 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
46 |
46 |
47 fun output_ml ctxt code_txt = |
47 fun output_ml ctxt code_txt = |
48 let |
48 let |
49 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) |
49 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) |
50 in |
50 in |
51 Pretty.str (Input.source_content code_txt) |
51 Pretty.str (fst (Input.source_content code_txt)) |
52 end |
52 end |
53 |
53 |
54 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close> |
54 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close> |
55 |
55 |
56 setup \<open>ml_checked_setup\<close> |
56 setup \<open>ml_checked_setup\<close> |
127 ellipses from it and replace them by @{text [quotes] "_"}. The following |
127 ellipses from it and replace them by @{text [quotes] "_"}. The following |
128 function will do this: |
128 function will do this: |
129 \<close> |
129 \<close> |
130 |
130 |
131 ML%linenosgray\<open>fun ml_pat pat code = |
131 ML%linenosgray\<open>fun ml_pat pat code = |
132 ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code\<close> |
132 ML_Lex.read "val" @ ML_Lex.read_source pat @ ML_Lex.read " = " @ ML_Lex.read_source code\<close> |
133 |
133 |
134 (* |
134 (* |
135 ML %grayML{*fun ml_pat code_txt pat = |
135 ML %grayML{*fun ml_pat code_txt pat = |
136 let val pat' = |
136 let val pat' = |
137 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
137 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
152 |
152 |
153 ML %linenosgray\<open> |
153 ML %linenosgray\<open> |
154 fun output_ml_resp ctxt (code_txt, pat) = |
154 fun output_ml_resp ctxt (code_txt, pat) = |
155 let |
155 let |
156 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) |
156 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) |
157 val code = space_explode "\n" (Input.source_content code_txt) |
157 val code = space_explode "\n" (fst (Input.source_content code_txt)) |
158 val resp = add_resp (space_explode "\n" (Input.source_content pat)) |
158 val resp = add_resp (space_explode "\n" (fst (Input.source_content pat))) |
159 in |
159 in |
160 Pretty.str (cat_lines (code @ resp)) |
160 Pretty.str (cat_lines (code @ resp)) |
161 end |
161 end |
162 |
162 |
163 val ml_response_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_resp"} (Scan.lift (Args.text_input -- Args.text_input)) output_ml_resp |
163 val ml_response_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_resp"} (Scan.lift (Args.text_input -- Args.text_input)) output_ml_resp |