44 |
44 |
45 val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
45 val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
46 |
46 |
47 text {* |
47 text {* |
48 |
48 |
49 Note that the parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
49 The parser @{ML "(Scan.lift Args.name)"} in line 9 parses a string, |
50 in this case the code. As mentioned before, the code |
50 in this case the code. As mentioned before, the code |
51 is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, |
51 is sent to the ML-compiler in the line 4 using the function @{ML ml_val}, |
52 which constructs the appropriate ML-expression. |
52 which constructs the appropriate ML-expression. |
53 If the code is ``approved'' by the compiler, then the output function @{ML |
53 If the code is ``approved'' by the compiler, then the output function @{ML |
54 "ThyOutput.output"} in the next line pretty prints the |
54 "ThyOutput.output"} in the next line pretty prints the |
55 code. This function expects that the code is a list of strings where each |
55 code. This function expects that the code is a list of (pretty)strings where each |
56 string correspond to a line in the output. Therefore the use of |
56 string correspond to a line in the output. Therefore the use of |
57 @{ML "(space_explode \"\\n\" txt)" for txt} |
57 @{ML "(space_explode \"\\n\" txt)" for txt} |
58 which produces this list according to linebreaks. There are a number of options |
58 which produces this list according to linebreaks. There are a number of options |
59 for antiquotations that are observed by @{ML ThyOutput.output} when printing the |
59 for antiquotations that are observed by @{ML ThyOutput.output} when printing the |
60 code (including @{text "[display]"} and @{text "[quotes]"}). Line 7 sets |
60 code (including @{text "[display]"} and @{text "[quotes]"}). Line 7 sets |
67 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
67 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
68 information about the line number, in case an error is detected. We |
68 information about the line number, in case an error is detected. We |
69 can improve the code above slightly by writing |
69 can improve the code above slightly by writing |
70 *} |
70 *} |
71 |
71 |
72 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt,pos) = |
72 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
73 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
73 (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt); |
74 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
74 ThyOutput.output (map Pretty.str (space_explode "\n" code_txt))) |
75 |
75 |
76 val _ = ThyOutput.antiquotation "ML_checked" |
76 val _ = ThyOutput.antiquotation "ML_checked" |
77 (Scan.lift (OuterParse.position Args.name)) output_ml *} |
77 (Scan.lift (OuterParse.position Args.name)) output_ml *} |
78 |
78 |
79 text {* |
79 text {* |
80 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. The |
|
81 parser @{ML OuterParse.position} encodes the positional information in the |
|
82 result. |
81 |
83 |
82 We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to |
84 We can now write in a document @{text "@{ML_checked \"2 + 3\"}"} in order to |
83 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
85 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
84 somebody changes the definition of \mbox{@{ML "(op +)"}}. |
86 somebody changes the definition of \mbox{@{ML "(op +)"}}. |
85 |
87 |