equal
deleted
inserted
replaced
31 "ML_Context.eval_in"} in Line 4 below). The complete code of the |
31 "ML_Context.eval_in"} in Line 4 below). The complete code of the |
32 antiquotation is as follows: |
32 antiquotation is as follows: |
33 |
33 |
34 *} |
34 *} |
35 |
35 |
36 ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt |
36 ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt |
37 |
37 |
38 fun output_ml src ctxt code_txt = |
38 fun output_ml src ctxt code_txt = |
39 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
39 (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); |
40 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
40 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
41 (space_explode "\n" code_txt)) |
41 (space_explode "\n" code_txt)) |
65 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
65 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
66 information about the line number, in case an error is detected. We |
66 information about the line number, in case an error is detected. We |
67 can improve the code above slightly by writing |
67 can improve the code above slightly by writing |
68 *} |
68 *} |
69 |
69 |
70 ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) = |
70 ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) = |
71 (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); |
72 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
72 ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt |
73 (space_explode "\n" code_txt)) |
73 (space_explode "\n" code_txt)) |
74 |
74 |
75 val _ = ThyOutput.add_commands |
75 val _ = ThyOutput.add_commands |