1 |
1 |
2 theory Antiquotes |
2 theory Antiquotes |
3 imports "../Appendix" |
3 imports "../Appendix" |
4 begin |
4 begin |
5 |
5 |
6 section {* Useful Document Antiquotations\label{rec:docantiquotations} *} |
6 section \<open>Useful Document Antiquotations\label{rec:docantiquotations}\<close> |
7 |
7 |
8 text {* |
8 text \<open> |
9 {\bf Problem:} |
9 {\bf Problem:} |
10 How to keep your ML-code inside a document synchronised with the actual code?\smallskip |
10 How to keep your ML-code inside a document synchronised with the actual code?\smallskip |
11 |
11 |
12 {\bf Solution:} This can be achieved with document antiquotations.\smallskip |
12 {\bf Solution:} This can be achieved with document antiquotations.\smallskip |
13 |
13 |
14 Document antiquotations can be used for ensuring consistent type-setting of |
14 Document antiquotations can be used for ensuring consistent type-setting of |
15 various entities in a document. They can also be used for sophisticated |
15 various entities in a document. They can also be used for sophisticated |
16 \LaTeX-hacking. If you type on the Isabelle level |
16 \LaTeX-hacking. If you type on the Isabelle level |
17 *} |
17 \<close> |
18 |
18 |
19 print_antiquotations |
19 print_antiquotations |
20 |
20 |
21 text {* |
21 text \<open> |
22 you obtain a list of all currently available document antiquotations and |
22 you obtain a list of all currently available document antiquotations and |
23 their options. |
23 their options. |
24 |
24 |
25 Below we will give the code for two additional document |
25 Below we will give the code for two additional document |
26 antiquotations both of which are intended to typeset ML-code. The crucial point |
26 antiquotations both of which are intended to typeset ML-code. The crucial point |
27 of these document antiquotations is that they not just print the ML-code, but also |
27 of these document antiquotations is that they not just print the ML-code, but also |
28 check whether it compiles. This will provide a sanity check for the code |
28 check whether it compiles. This will provide a sanity check for the code |
29 and also allows you to keep documents in sync with other code, for example |
29 and also allows you to keep documents in sync with other code, for example |
30 Isabelle. |
30 Isabelle. |
31 |
31 |
32 We first describe the antiquotation @{text "ML_checked"} with the syntax: |
32 We first describe the antiquotation \<open>ML_checked\<close> with the syntax: |
33 |
33 |
34 @{text [display] "@{ML_checked \"a_piece_of_code\"}"} |
34 @{text [display] "@{ML_checked \"a_piece_of_code\"}"} |
35 |
35 |
36 The code is checked by sending the ML-expression @{text [quotes] "val _ = |
36 The code is checked by sending the ML-expression @{text [quotes] "val _ = |
37 a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML |
37 a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML |
38 "ML_Context.eval_source_in"} in Line 7 below). The complete code of the |
38 "ML_Context.eval_source_in"} in Line 7 below). The complete code of the |
39 document antiquotation is as follows: |
39 document antiquotation is as follows: |
40 |
40 |
41 *} |
41 \<close> |
42 ML \<open>Input.pos_of\<close> |
42 ML \<open>Input.pos_of\<close> |
43 ML%linenosgray{*fun ml_enclose bg en source = |
43 ML%linenosgray\<open>fun ml_enclose bg en source = |
44 ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;*} |
44 ML_Lex.read bg @ ML_Lex.read_source false source @ ML_Lex.read en;\<close> |
45 |
45 |
46 ML%linenosgray{*fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
46 ML%linenosgray\<open>fun ml_val code_txt = (ml_enclose "val _ = " "" code_txt) |
47 |
47 |
48 fun output_ml ctxt code_txt = |
48 fun output_ml ctxt code_txt = |
49 let |
49 let |
50 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) |
50 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_val code_txt) |
51 in |
51 in |
52 Pretty.str (Input.source_content code_txt) |
52 Pretty.str (Input.source_content code_txt) |
53 end |
53 end |
54 |
54 |
55 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml*} |
55 val ml_checked_setup = Thy_Output.antiquotation_pretty_source @{binding "ML_checked"} (Scan.lift Args.text_input) output_ml\<close> |
56 |
56 |
57 setup {* ml_checked_setup *} |
57 setup \<open>ml_checked_setup\<close> |
58 |
58 |
59 |
59 |
60 text {* |
60 text \<open> |
61 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
61 The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this |
62 case the code, and then calls the function @{ML output_ml}. As mentioned |
62 case the code, and then calls the function @{ML output_ml}. As mentioned |
63 before, the parsed code is sent to the ML-compiler in Line 4 using the |
63 before, the parsed code is sent to the ML-compiler in Line 4 using the |
64 function @{ML ml_val}, which constructs the appropriate ML-expression, and |
64 function @{ML ml_val}, which constructs the appropriate ML-expression, and |
65 using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is |
65 using @{ML "eval_in" in ML_Context}, which calls the compiler. If the code is |
67 Document_Antiquotation} in the next line pretty prints the code. This function expects |
67 Document_Antiquotation} in the next line pretty prints the code. This function expects |
68 that the code is a list of (pretty)strings where each string correspond to a |
68 that the code is a list of (pretty)strings where each string correspond to a |
69 line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" |
69 line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)" |
70 for txt} which produces such a list according to linebreaks. There are a |
70 for txt} which produces such a list according to linebreaks. There are a |
71 number of options for antiquotations that are observed by the function |
71 number of options for antiquotations that are observed by the function |
72 @{ML "output" in Document_Antiquotation} when printing the code (including @{text "[display]"} |
72 @{ML "output" in Document_Antiquotation} when printing the code (including \<open>[display]\<close> |
73 and @{text "[quotes]"}). The function @{ML "antiquotation_raw" in Thy_Output} in |
73 and \<open>[quotes]\<close>). The function @{ML "antiquotation_raw" in Thy_Output} in |
74 Line 7 sets up the new document antiquotation. |
74 Line 7 sets up the new document antiquotation. |
75 |
75 |
76 \begin{readmore} |
76 \begin{readmore} |
77 For more information about options of document antiquotations see \rsccite{sec:antiq}). |
77 For more information about options of document antiquotations see \rsccite{sec:antiq}). |
78 \end{readmore} |
78 \end{readmore} |
79 |
79 |
80 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
80 Since we used the argument @{ML "Position.none"}, the compiler cannot give specific |
81 information about the line number, in case an error is detected. We |
81 information about the line number, in case an error is detected. We |
82 can improve the code above slightly by writing |
82 can improve the code above slightly by writing |
83 *} |
83 \<close> |
84 (* FIXME: remove |
84 (* FIXME: remove |
85 ML%linenosgray{*fun output_ml ctxt (code_txt, pos) = |
85 ML%linenosgray{*fun output_ml ctxt (code_txt, pos) = |
86 let |
86 let |
87 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
87 val srcpos = {delimited = false, pos = pos, text = ml_val code_txt} |
88 in |
88 in |
98 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
98 val ml_checked_setup2 = Thy_Output.antiquotation @{binding "ML_checked2"} |
99 (Scan.lift (Parse.position Args.name)) output_ml *} |
99 (Scan.lift (Parse.position Args.name)) output_ml *} |
100 |
100 |
101 setup {* ml_checked_setup2 *} |
101 setup {* ml_checked_setup2 *} |
102 *) |
102 *) |
103 text {* |
103 text \<open> |
104 where in Lines 1 and 2 the positional information is properly treated. The |
104 where in Lines 1 and 2 the positional information is properly treated. The |
105 parser @{ML Parse.position} encodes the positional information in the |
105 parser @{ML Parse.position} encodes the positional information in the |
106 result. |
106 result. |
107 |
107 |
108 We can now write @{text "@{ML_checked2 \"2 + 3\"}"} in a document in order to |
108 We can now write \<open>@{ML_checked2 "2 + 3"}\<close> in a document in order to |
109 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
109 obtain @{ML_checked "2 + 3"} and be sure that this code compiles until |
110 somebody changes the definition of addition. |
110 somebody changes the definition of addition. |
111 |
111 |
112 |
112 |
113 The second document antiquotation we describe extends the first by a pattern |
113 The second document antiquotation we describe extends the first by a pattern |
117 |
117 |
118 |
118 |
119 @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"} |
119 @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"} |
120 |
120 |
121 To add some convenience and also to deal with large outputs, the user can |
121 To add some convenience and also to deal with large outputs, the user can |
122 give a partial specification by using ellipses. For example @{text "(\<dots>, \<dots>)"} |
122 give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close> |
123 for specifying a pair. In order to check consistency between the pattern |
123 for specifying a pair. In order to check consistency between the pattern |
124 and the output of the code, we have to change the ML-expression that is sent |
124 and the output of the code, we have to change the ML-expression that is sent |
125 to the compiler: in @{text "ML_checked2"} we sent the expression @{text [quotes] |
125 to the compiler: in \<open>ML_checked2\<close> we sent the expression @{text [quotes] |
126 "val _ = a_piece_of_code"} to the compiler; now the wildcard @{text "_"} |
126 "val _ = a_piece_of_code"} to the compiler; now the wildcard \<open>_\<close> |
127 must be be replaced by the given pattern. However, we have to remove all |
127 must be be replaced by the given pattern. However, we have to remove all |
128 ellipses from it and replace them by @{text [quotes] "_"}. The following |
128 ellipses from it and replace them by @{text [quotes] "_"}. The following |
129 function will do this: |
129 function will do this: |
130 *} |
130 \<close> |
131 |
131 |
132 ML%linenosgray{*fun ml_pat pat code = |
132 ML%linenosgray\<open>fun ml_pat pat code = |
133 ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code*} |
133 ML_Lex.read "val" @ ML_Lex.read_source false pat @ ML_Lex.read " = " @ ML_Lex.read_source false code\<close> |
134 |
134 |
135 (* |
135 (* |
136 ML %grayML{*fun ml_pat code_txt pat = |
136 ML %grayML{*fun ml_pat code_txt pat = |
137 let val pat' = |
137 let val pat' = |
138 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
138 implode (map (fn "\<dots>" => "_" | s => s) (Symbol.explode pat)) |
139 in |
139 in |
140 ml_enclose ("val " ^ pat' ^ " = ") "" code_txt |
140 ml_enclose ("val " ^ pat' ^ " = ") "" code_txt |
141 end*} |
141 end*} |
142 *) |
142 *) |
143 text {* |
143 text \<open> |
144 Next we add a response indicator to the result using: |
144 Next we add a response indicator to the result using: |
145 *} |
145 \<close> |
146 |
146 |
147 |
147 |
148 ML %grayML{*fun add_resp pat = map (fn s => "> " ^ s) pat*} |
148 ML %grayML\<open>fun add_resp pat = map (fn s => "> " ^ s) pat\<close> |
149 |
149 |
150 text {* |
150 text \<open> |
151 The rest of the code of @{text "ML_resp"} is: |
151 The rest of the code of \<open>ML_resp\<close> is: |
152 *} |
152 \<close> |
153 |
153 |
154 ML %linenosgray\<open> |
154 ML %linenosgray\<open> |
155 fun output_ml_resp ctxt (code_txt, pat) = |
155 fun output_ml_resp ctxt (code_txt, pat) = |
156 let |
156 let |
157 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) |
157 val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of code_txt) (ml_pat pat code_txt) |
182 |
182 |
183 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
183 val ml_resp_setup = Thy_Output.antiquotation @{binding "ML_resp"} |
184 (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) |
184 (Scan.lift (Parse.position (Args.text_input -- Args.text_input))) |
185 output_ml_resp*} |
185 output_ml_resp*} |
186 *) |
186 *) |
187 setup {* ml_response_setup *} |
187 setup \<open>ml_response_setup\<close> |
188 |
188 |
189 (* FIXME *) |
189 (* FIXME *) |
190 text {* |
190 text \<open> |
191 In comparison with @{text "ML_checked"}, we only changed the line about |
191 In comparison with \<open>ML_checked\<close>, we only changed the line about |
192 the compiler (Line~2), the lines about |
192 the compiler (Line~2), the lines about |
193 the output (Lines 4 to 7) and the parser in the setup (Line 11). Now |
193 the output (Lines 4 to 7) and the parser in the setup (Line 11). Now |
194 you can write |
194 you can write |
195 |
195 |
196 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |
196 @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"} |