equal
deleted
inserted
replaced
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_in (SOME ctxt) false pos (ml_val code_txt); |
78 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
78 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
79 |
79 |
80 val _ = ThyOutput.antiquotation "ML_checked" |
80 val _ = ThyOutput.antiquotation "ML_checked" |
81 (Scan.lift (OuterParse.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 OuterParse.position} encodes the positional information in the |
85 parser @{ML Parse.position} encodes the positional information in the |
86 result. |
86 result. |
87 |
87 |
88 We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to |
88 We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to |
89 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
89 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
90 somebody changes the definition of addition. |
90 somebody changes the definition of addition. |
135 in |
135 in |
136 ThyOutput.output (map Pretty.str (code_output @ resp_output)) |
136 ThyOutput.output (map Pretty.str (code_output @ resp_output)) |
137 end) |
137 end) |
138 |
138 |
139 val _ = ThyOutput.antiquotation "ML_resp" |
139 val _ = ThyOutput.antiquotation "ML_resp" |
140 (Scan.lift (OuterParse.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 |
145 the compiler (Line~2), the lines about |
145 the compiler (Line~2), the lines about |