30 given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} |
30 given argument to the ML-compiler (i.e.~the function @{ML "ML_Context.eval_in"} |
31 in Line 4 below). The complete code of the antiquotation is as follows: |
31 in Line 4 below). The complete code of the antiquotation is as follows: |
32 |
32 |
33 *} |
33 *} |
34 |
34 |
35 ML %linenumbers {*fun ml_val code_txt = "val _ = " ^ code_txt |
35 ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt |
36 |
36 |
37 fun output_ml src ctxt code_txt = |
37 fun output_ml src ctxt code_txt = |
38 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
38 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
39 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
39 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
40 (space_explode "\n" code_txt)) |
40 (space_explode "\n" code_txt)) |
41 |
41 |
42 val _ = ThyOutput.add_commands |
42 val _ = ThyOutput.add_commands |
43 [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)] |
43 [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*} |
44 *} |
|
45 |
44 |
46 text {* |
45 text {* |
47 |
46 |
48 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
47 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
49 in this case the code given as argument. As mentioned before, this argument |
48 in this case the code given as argument. As mentioned before, this argument |
66 information about the line number, in case an error is detected. We |
65 information about the line number, in case an error is detected. We |
67 can improve the code above slightly by writing |
66 can improve the code above slightly by writing |
68 |
67 |
69 *} |
68 *} |
70 |
69 |
71 ML %linenumbers {* fun output_ml src ctxt (code_txt,pos) = |
70 ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) = |
72 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
71 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
73 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
72 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
74 (space_explode "\n" code_txt)) |
73 (space_explode "\n" code_txt)) |
75 |
74 |
76 val _ = ThyOutput.add_commands |
75 val _ = ThyOutput.add_commands |
77 [("ML_checked", ThyOutput.args |
76 [("ML_checked", ThyOutput.args |
78 (Scan.lift (OuterParse.position Args.name)) output_ml)] |
77 (Scan.lift (OuterParse.position Args.name)) output_ml)] *} |
79 *} |
|
80 |
78 |
81 text {* |
79 text {* |
82 where in Lines 1 and 2 the positional information is properly treated. |
80 where in Lines 1 and 2 the positional information is properly treated. |
83 |
81 |
84 (FIXME: say something about OuterParse.position) |
82 (FIXME: say something about OuterParse.position) |
105 do this we need to replace the @{text [quotes] "\<dots>"} by @{text [quotes] "_"} |
103 do this we need to replace the @{text [quotes] "\<dots>"} by @{text [quotes] "_"} |
106 before sending the code to the compiler. The following function will do this: |
104 before sending the code to the compiler. The following function will do this: |
107 |
105 |
108 *} |
106 *} |
109 |
107 |
110 ML {* |
108 ML{*fun ml_pat (code_txt, pat) = |
111 fun ml_pat (code_txt, pat) = |
|
112 let val pat' = |
109 let val pat' = |
113 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
110 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
114 in |
111 in |
115 "val " ^ pat' ^ " = " ^ code_txt |
112 "val " ^ pat' ^ " = " ^ code_txt |
116 end |
113 end*} |
117 *} |
|
118 |
114 |
119 text {* |
115 text {* |
120 Next we like to add a response indicator to the result using: |
116 Next we like to add a response indicator to the result using: |
121 *} |
117 *} |
122 |
118 |
123 |
119 |
124 ML {* |
120 ML{*fun add_response_indicator pat = |
125 fun add_response_indicator pat = |
121 map (fn s => "> " ^ s) (space_explode "\n" pat) *} |
126 map (fn s => "> " ^ s) (space_explode "\n" pat) |
|
127 *} |
|
128 |
122 |
129 text {* |
123 text {* |
130 The rest of the code of the antiquotation is |
124 The rest of the code of the antiquotation is |
131 *} |
125 *} |
132 |
126 |
133 ML {* |
127 ML{*fun output_ml_response src ctxt ((code_txt,pat),pos) = |
134 fun output_ml_response src ctxt ((code_txt,pat),pos) = |
|
135 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
128 (ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat)); |
136 let |
129 let |
137 val output = (space_explode "\n" code_txt) @ (add_response_indicator pat) |
130 val output = (space_explode "\n" code_txt) @ (add_response_indicator pat) |
138 in |
131 in |
139 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output |
132 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output |
141 |
134 |
142 val _ = ThyOutput.add_commands |
135 val _ = ThyOutput.add_commands |
143 [("ML_response", |
136 [("ML_response", |
144 ThyOutput.args |
137 ThyOutput.args |
145 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
138 (Scan.lift (OuterParse.position (Args.name -- Args.name))) |
146 output_ml_response)] |
139 output_ml_response)]*} |
147 *} |
|
148 |
140 |
149 text {* |
141 text {* |
150 This extended antiquotation allows us to write |
142 This extended antiquotation allows us to write |
151 @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"} |
143 @{text [display] "@{ML_response [display] \"true andalso false\" \"false\"}"} |
152 to obtain |
144 to obtain |