33 |
33 |
34 @{text [display] "@{ML_checked \"a_piece_of_code\"}"} |
34 @{text [display] "@{ML_checked \"a_piece_of_code\"}"} |
35 |
35 |
36 The code is checked by sending the ML-expression @{text [quotes] "val _ = |
36 The code is checked by sending the ML-expression @{text [quotes] "val _ = |
37 a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML |
37 a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML |
38 "ML_Context.eval_text_in"} in Line 4 below). The complete code of the |
38 "ML_Context.eval_source_in"} in Line 7 below). The complete code of the |
39 document antiquotation is as follows: |
39 document antiquotation is as follows: |
40 |
40 |
41 *} |
41 *} |
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 let |
|
47 val srcpos = {delimited = false, text = (ml_val code_txt), pos = Position.none} |
|
48 in |
|
49 (ML_Context.eval_source_in (SOME ctxt) false srcpos; |
47 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 |
48 |
52 |
49 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*} |
50 |
54 |
51 setup {* ml_checked_setup *} |
55 setup {* ml_checked_setup *} |
52 |
56 |
74 information about the line number, in case an error is detected. We |
78 information about the line number, in case an error is detected. We |
75 can improve the code above slightly by writing |
79 can improve the code above slightly by writing |
76 *} |
80 *} |
77 |
81 |
78 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
82 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
79 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
83 let |
|
84 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
|
85 in |
|
86 (ML_Context.eval_source_in (SOME ctxt) false srcpos; |
80 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 |
81 |
89 |
82 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
90 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
83 (Scan.lift (Parse.position Args.name)) output_ml *} |
91 (Scan.lift (Parse.position Args.name)) output_ml *} |
84 |
92 |
85 setup {* ml_checked_setup2 *} |
93 setup {* ml_checked_setup2 *} |
130 text {* |
138 text {* |
131 The rest of the code of @{text "ML_resp"} is: |
139 The rest of the code of @{text "ML_resp"} is: |
132 *} |
140 *} |
133 |
141 |
134 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) = |
135 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_pat (code_txt, pat)); |
143 (let |
|
144 val srcpos = {delimited = false, text = ml_pat (code_txt, pat), pos = pos} |
|
145 in |
|
146 ML_Context.eval_source_in (SOME ctxt) false srcpos |
|
147 end; |
136 let |
148 let |
137 val code_output = space_explode "\n" code_txt |
149 val code_output = space_explode "\n" code_txt |
138 val resp_output = add_resp (space_explode "\n" pat) |
150 val resp_output = add_resp (space_explode "\n" pat) |
139 in |
151 in |
140 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
152 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
141 end) |
153 end) |
|
154 |
142 |
155 |
143 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
156 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
144 (Scan.lift (Parse.position (Args.name -- Args.name))) |
157 (Scan.lift (Parse.position (Args.name -- Args.name))) |
145 output_ml_resp*} |
158 output_ml_resp*} |
146 |
159 |