44 |
44 |
45 fun output_ml {context = ctxt, ...} code_txt = |
45 fun output_ml {context = ctxt, ...} code_txt = |
46 (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); |
46 (ML_Context.eval_text_in (SOME ctxt) false Position.none (ml_val code_txt); |
47 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
47 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
48 |
48 |
49 val _ = Thy_Output.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*} |
49 val ml_checked_setup = Thy_Output.antiquotation @{binding "ML_checked"} (Scan.lift Args.name) output_ml*} |
|
50 |
|
51 setup {* ml_checked_setup *} |
50 |
52 |
51 text {* |
53 text {* |
52 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
54 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
53 case the code, and then calls the function @{ML output_ml}. As mentioned |
55 case the code, and then calls the function @{ML output_ml}. As mentioned |
54 before, the parsed code is sent to the ML-compiler in Line 4 using the |
56 before, the parsed code is sent to the ML-compiler in Line 4 using the |
75 |
77 |
76 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
78 ML%linenosgray{*fun output_ml {context = ctxt, ...} (code_txt, pos) = |
77 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
79 (ML_Context.eval_text_in (SOME ctxt) false pos (ml_val code_txt); |
78 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
80 Thy_Output.output ctxt (map Pretty.str (space_explode "\n" code_txt))) |
79 |
81 |
80 val _ = Thy_Output.antiquotation "ML_checked" |
82 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
81 (Scan.lift (Parse.position Args.name)) output_ml *} |
83 (Scan.lift (Parse.position Args.name)) output_ml *} |
|
84 |
|
85 setup {* ml_checked_setup2 *} |
82 |
86 |
83 text {* |
87 text {* |
84 where in Lines 1 and 2 the positional information is properly treated. The |
88 where in Lines 1 and 2 the positional information is properly treated. The |
85 parser @{ML Parse.position} encodes the positional information in the |
89 parser @{ML Parse.position} encodes the positional information in the |
86 result. |
90 result. |
87 |
91 |
88 We can now write @{text "@{ML_checked \"2 + 3\"}"} in a document in order to |
92 We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to |
89 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
93 obtain @{ML_checked2 "2 + 3"} and be sure that this code compiles until |
90 somebody changes the definition of addition. |
94 somebody changes the definition of addition. |
91 |
95 |
92 |
96 |
93 The second document antiquotation we describe extends the first by a pattern |
97 The second document antiquotation we describe extends the first by a pattern |
94 that specifies what the result of the ML-code should be and checks the |
98 that specifies what the result of the ML-code should be and checks the |
100 |
104 |
101 To add some convenience and also to deal with large outputs, the user can |
105 To add some convenience and also to deal with large outputs, the user can |
102 give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"} |
106 give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"} |
103 for specifying a pair. In order to check consistency between the pattern |
107 for specifying a pair. In order to check consistency between the pattern |
104 and the output of the code, we have to change the ML-expression that is sent |
108 and the output of the code, we have to change the ML-expression that is sent |
105 to the compiler: in @{text "ML_checked"} we sent the expression @{text [quotes] |
109 to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes] |
106 "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"} |
110 "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"} |
107 must be be replaced by the given pattern. However, we have to remove all |
111 must be be replaced by the given pattern. However, we have to remove all |
108 ellipses from it and replace them by @{text [quotes] "_"}. The following |
112 ellipses from it and replace them by @{text [quotes] "_"}. The following |
109 function will do this: |
113 function will do this: |
110 *} |
114 *} |
134 val resp_output = add_resp (space_explode "\n" pat) |
138 val resp_output = add_resp (space_explode "\n" pat) |
135 in |
139 in |
136 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
140 Thy_Output.output ctxt (map Pretty.str (code_output @ resp_output)) |
137 end) |
141 end) |
138 |
142 |
139 val _ = Thy_Output.antiquotation "ML_resp" |
143 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
140 (Scan.lift (Parse.position (Args.name -- Args.name))) |
144 (Scan.lift (Parse.position (Args.name -- Args.name))) |
141 output_ml_resp*} |
145 output_ml_resp*} |
142 |
146 |
|
147 setup {* ml_resp_setup *} |
|
148 |
143 text {* |
149 text {* |
144 In comparison with @{text "ML_checked"}, we only changed the line about |
150 In comparison with @{text "ML_checked2"}, we only changed the line about |
145 the compiler (Line~2), the lines about |
151 the compiler (Line~2), the lines about |
146 the output (Lines 4 to 7) and the parser in the setup (Line 11). Now |
152 the output (Lines 4 to 7) and the parser in the setup (Line 11). Now |
147 you can write |
153 you can write |
148 |
154 |
149 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |
155 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |