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_in"} in Line 4 below). The complete code of the |
38 "ML_Context.eval_text_in"} in Line 4 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_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 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
47 Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) |
48 |
48 |
49 val _ = ThyOutput.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 |
53 case the code, and then calls the function @{ML output_ml}. As mentioned |
53 case the code, and then calls the function @{ML output_ml}. As mentioned |
54 before, the parsed code is sent to the ML-compiler in Line 4 using the |
54 before, the parsed code is sent to the ML-compiler in Line 4 using the |
55 function @{ML ml_val}, which constructs the appropriate ML-expression, and |
55 function @{ML ml_val}, which constructs the appropriate ML-expression, and |
56 using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is |
56 using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is |
57 ``approved'' by the compiler, then the output function @{ML "output" in |
57 ``approved'' by the compiler, then the output function @{ML "output" in |
58 ThyOutput} in the next line pretty prints the code. This function expects |
58 Thy_Output} in the next line pretty prints the code. This function expects |
59 that the code is a list of (pretty)strings where each string correspond to a |
59 that the code is a list of (pretty)strings where each string correspond to a |
60 line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" |
60 line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" |
61 for txt} which produces such a list according to linebreaks. There are a |
61 for txt} which produces such a list according to linebreaks. There are a |
62 number of options for antiquotations that are observed by the function |
62 number of options for antiquotations that are observed by the function |
63 @{ML "output" in ThyOutput} when printing the code (including @{text "[display]"} |
63 @{ML "output" in Thy_Output} when printing the code (including @{text "[display]"} |
64 and @{text "[quotes]"}). The function @{ML "antiquotation" in ThyOutput} in |
64 and @{text "[quotes]"}). The function @{ML "antiquotation" in Thy_Output} in |
65 Line 7 sets up the new document antiquotation. |
65 Line 7 sets up the new document antiquotation. |
66 |
66 |
67 \begin{readmore} |
67 \begin{readmore} |
68 For more information about options of document antiquotations see \rsccite{sec:antiq}). |
68 For more information about options of document antiquotations see \rsccite{sec:antiq}). |
69 \end{readmore} |
69 \end{readmore} |
72 information about the line number, in case an error is detected. We |
72 information about the line number, in case an error is detected. We |
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_in (SOME ctxt) false pos (ml_val code_txt); |
77 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
78 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
78 Thy_Output.output (map Pretty.str (space_explode "\n" code_txt))) |
79 |
79 |
80 val _ = ThyOutput.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 {* |
84 where in Lines 1 and 2 the positional information is properly treated. The |
84 where in Lines 1 and 2 the positional information is properly treated. The |
85 parser @{ML Parse.position} encodes the positional information in the |
85 parser @{ML Parse.position} encodes the positional information in the |
126 text {* |
126 text {* |
127 The rest of the code of @{text "ML_resp"} is: |
127 The rest of the code of @{text "ML_resp"} is: |
128 *} |
128 *} |
129 |
129 |
130 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = |
130 ML %linenosgray{*fun output_ml_resp {context = ctxt, ...} ((code_txt, pat), pos) = |
131 (ML_Context.eval_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 ThyOutput.output (map Pretty.str (code_output @ resp_output)) |
136 Thy_Output.output (map Pretty.str (code_output @ resp_output)) |
137 end) |
137 end) |
138 |
138 |
139 val _ = ThyOutput.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*} |
142 |
142 |
143 text {* |
143 text {* |
144 In comparison with @{text "ML_checked"}, we only changed the line about |
144 In comparison with @{text "ML_checked"}, we only changed the line about |