34 "ML_Context.eval_in"} in Line 4 below). The complete code of the |
34 "ML_Context.eval_in"} in Line 4 below). The complete code of the |
35 antiquotation is as follows: |
35 antiquotation is as follows: |
36 |
36 |
37 *} |
37 *} |
38 |
38 |
|
39 ML {* Pretty.str *} |
|
40 |
39 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt |
41 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt |
40 |
42 |
41 fun output_ml src ctxt code_txt = |
43 fun output_ml {source = src, context = ctxt, ...} code_txt = |
42 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
44 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
43 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
45 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
44 (space_explode "\n" code_txt)) |
|
45 |
46 |
46 val _ = ThyOutput.add_commands |
47 val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
47 [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*} |
|
48 |
48 |
49 text {* |
49 text {* |
50 |
50 |
51 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
51 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
52 in this case the code given as argument. As mentioned before, this argument |
52 in this case the code given as argument. As mentioned before, this argument |
53 is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, |
53 is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, |
54 which constructs the appropriate ML-expression. |
54 which constructs the appropriate ML-expression. |
55 If the code is ``approved'' by the compiler, then the output function @{ML |
55 If the code is ``approved'' by the compiler, then the output function @{ML |
56 "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the |
56 "ThyOutput.output"} in the next line pretty prints the |
57 code. This function expects that the code is a list of strings where each |
57 code. This function expects that the code is a list of strings where each |
58 string correspond to a line in the output. Therefore the use of |
58 string correspond to a line in the output. Therefore the use of |
59 @{ML "(space_explode \"\\n\" txt)" for txt} |
59 @{ML "(space_explode \"\\n\" txt)" for txt} |
60 which produces this list according to linebreaks. There are a number of options for antiquotations |
60 which produces this list according to linebreaks. There are a number of options |
61 that are observed by @{ML ThyOutput.output_list} when printing the code (including |
61 for antiquotations that are observed by @{ML ThyOutput.output} when printing the |
62 @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}). |
62 code (including @{text "[display]"} and @{text "[quotes]"}). |
63 |
63 |
64 \begin{readmore} |
64 \begin{readmore} |
65 For more information about options of antiquotations see \rsccite{sec:antiq}). |
65 For more information about options of antiquotations see \rsccite{sec:antiq}). |
66 \end{readmore} |
66 \end{readmore} |
67 |
67 |
68 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
68 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
69 information about the line number, in case an error is detected. We |
69 information about the line number, in case an error is detected. We |
70 can improve the code above slightly by writing |
70 can improve the code above slightly by writing |
71 *} |
71 *} |
72 |
72 |
73 ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) = |
73 ML%linenosgray{*fun output_ml {source = src, context = ctxt, ...} (code_txt,pos) = |
74 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
74 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
75 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
75 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
76 (space_explode "\n" code_txt)) |
|
77 |
76 |
78 val _ = ThyOutput.add_commands |
77 val _ = ThyOutput.antiquotation "ML_checked" |
79 [("ML_checked", ThyOutput.args |
78 (Scan.lift (OuterParse.position Args.name)) output_ml *} |
80 (Scan.lift (OuterParse.position Args.name)) output_ml)] *} |
|
81 |
79 |
82 text {* |
80 text {* |
83 where in Lines 1 and 2 the positional information is properly treated. |
81 where in Lines 1 and 2 the positional information is properly treated. |
84 |
82 |
85 (FIXME: say something about OuterParse.position) |
83 (FIXME: say something about OuterParse.position) |
127 |
125 |
128 text {* |
126 text {* |
129 The rest of the code of the antiquotation is |
127 The rest of the code of the antiquotation is |
130 *} |
128 *} |
131 |
129 |
132 ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) = |
130 ML{*fun output_ml_resp {source = src, context = ctxt, ...} ((code_txt,pat),pos) = |
133 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
131 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
134 let |
132 let |
135 val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat) |
133 val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat) |
136 in |
134 in |
137 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output |
135 ThyOutput.output (map Pretty.str output) |
138 end) |
136 end) |
139 |
137 |
140 val _ = ThyOutput.add_commands |
138 val _ = ThyOutput.antiquotation "ML_resp" |
141 [("ML_resp", |
139 (Scan.lift (OuterParse.position (Args.name -- Args.name))) output_ml_resp*} |
142 ThyOutput.args |
|
143 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
|
144 output_ml_resp)]*} |
|
145 |
140 |
146 text {* |
141 text {* |
147 This extended antiquotation allows us to write |
142 This extended antiquotation allows us to write |
148 |
143 |
149 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |
144 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |