20 four \LaTeX{} commands are defined: |
20 four \LaTeX{} commands are defined: |
21 |
21 |
22 \begin{center} |
22 \begin{center} |
23 \begin{tabular}{l|c|c} |
23 \begin{tabular}{l|c|c} |
24 & Chapters & Sections\\\hline |
24 & Chapters & Sections\\\hline |
25 Implementation Manual & @{text "\\ichcite{\<dots>}"} & @{text "\\isccite{\<dots>}"}\\ |
25 Implementation Manual & \<open>\ichcite{\<dots>}\<close> & \<open>\isccite{\<dots>}\<close>\\ |
26 Isar Reference Manual & @{text "\\rchcite{\<dots>}"} & @{text "\\rsccite{\<dots>}"}\\ |
26 Isar Reference Manual & \<open>\rchcite{\<dots>}\<close> & \<open>\rsccite{\<dots>}\<close>\\ |
27 \end{tabular} |
27 \end{tabular} |
28 \end{center} |
28 \end{center} |
29 |
29 |
30 So @{text "\\ichcite{ch:logic}"} yields a reference for the chapter about logic |
30 So \<open>\ichcite{ch:logic}\<close> yields a reference for the chapter about logic |
31 in the implementation manual, namely \ichcite{ch:logic}. |
31 in the implementation manual, namely \ichcite{ch:logic}. |
32 |
32 |
33 \item There are various document antiquotations defined for the |
33 \item There are various document antiquotations defined for the |
34 tutorial. They allow to check the written text against the current |
34 tutorial. They allow to check the written text against the current |
35 Isabelle code and also allow to show responses of the ML-compiler. |
35 Isabelle code and also allow to show responses of the ML-compiler. |
37 appropriate. |
37 appropriate. |
38 |
38 |
39 The following antiquotations are defined: |
39 The following antiquotations are defined: |
40 |
40 |
41 \begin{itemize} |
41 \begin{itemize} |
42 \item[$\bullet$] @{text "@{ML \"expr\" for vars in structs}"} should be used |
42 \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used |
43 for displaying any ML-ex\-pression, because the antiquotation checks whether |
43 for displaying any ML-ex\-pression, because the antiquotation checks whether |
44 the expression is valid ML-code. The @{text "for"}- and @{text |
44 the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open |
45 "in"}-arguments are optional. The former is used for evaluating open |
|
46 expressions by giving a list of free variables. The latter is used to |
45 expressions by giving a list of free variables. The latter is used to |
47 indicate in which structure or structures the ML-expression should be |
46 indicate in which structure or structures the ML-expression should be |
48 evaluated. Examples are: |
47 evaluated. Examples are: |
49 |
48 |
50 \begin{center}\small |
49 \begin{center}\small |
51 \begin{tabular}{lll} |
50 \begin{tabular}{lll} |
52 @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ |
51 \<open>@{ML "1 + 3"}\<close> & & @{ML "1 + 3"}\\ |
53 @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
52 \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
54 @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ |
53 \<open>@{ML Ident in OuterLex}\<close> & & @{ML Ident in OuterLex}\\ |
55 \end{tabular} |
54 \end{tabular} |
56 \end{center} |
55 \end{center} |
57 |
56 |
58 \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to |
57 \item[$\bullet$] \<open>@{ML_response "expr" "pat"}\<close> should be used to |
59 display ML-expressions and their response. The first expression is checked |
58 display ML-expressions and their response. The first expression is checked |
60 like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern |
59 like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern |
61 that specifies the result the first expression produces. This pattern can |
60 that specifies the result the first expression produces. This pattern can |
62 contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the |
61 contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the |
63 first expression will be checked against this pattern. Examples are: |
62 first expression will be checked against this pattern. Examples are: |
64 |
63 |
65 \begin{center}\small |
64 \begin{center}\small |
66 \begin{tabular}{l} |
65 \begin{tabular}{l} |
67 @{text "@{ML_response \"1+2\" \"3\"}"}\\ |
66 \<open>@{ML_response "1+2" "3"}\<close>\\ |
68 @{text "@{ML_response \"(1+2,3)\" \"(3,\<dots>)\"}"} |
67 \<open>@{ML_response "(1+2,3)" "(3,\<dots>)"}\<close> |
69 \end{tabular} |
68 \end{tabular} |
70 \end{center} |
69 \end{center} |
71 |
70 |
72 which produce respectively |
71 which produce respectively |
73 |
72 |
80 |
79 |
81 Note that this antiquotation can only be used when the result can be |
80 Note that this antiquotation can only be used when the result can be |
82 constructed: it does not work when the code produces an exception or returns |
81 constructed: it does not work when the code produces an exception or returns |
83 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
82 an abstract datatype (like @{ML_type thm} or @{ML_type cterm}). |
84 |
83 |
85 \item[$\bullet$] @{text "@{ML_response_fake \"expr\" \"pat\"}"} works just |
84 \item[$\bullet$] \<open>@{ML_response_fake "expr" "pat"}\<close> works just |
86 like the antiquotation @{text "@{ML_response \"expr\" \"pat\"}"} above, |
85 like the antiquotation \<open>@{ML_response "expr" "pat"}\<close> above, |
87 except that the result-specification is not checked. Use this antiquotation |
86 except that the result-specification is not checked. Use this antiquotation |
88 when the result cannot be constructed or the code generates an |
87 when the result cannot be constructed or the code generates an |
89 exception. Examples are: |
88 exception. Examples are: |
90 |
89 |
91 \begin{center}\small |
90 \begin{center}\small |
92 \begin{tabular}{ll} |
91 \begin{tabular}{ll} |
93 @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ |
92 \<open>@{ML_response_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\ |
94 & @{text "\"a + b = c\"}"}\smallskip\\ |
93 & \<open>"a + b = c"}\<close>\smallskip\\ |
95 @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ |
94 \<open>@{ML_response_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ |
96 & @{text "\"Exception FAIL raised\"}"} |
95 & \<open>"Exception FAIL raised"}\<close> |
97 \end{tabular} |
96 \end{tabular} |
98 \end{center} |
97 \end{center} |
99 |
98 |
100 which produce respectively |
99 which produce respectively |
101 |
100 |
107 \end{center} |
106 \end{center} |
108 |
107 |
109 This output mimics to some extend what the user sees when running the |
108 This output mimics to some extend what the user sees when running the |
110 code. |
109 code. |
111 |
110 |
112 \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be |
111 \item[$\bullet$] \<open>@{ML_response_fake_both "expr" "pat"}\<close> can be |
113 used to show erroneous code. Neither the code nor the response will be |
112 used to show erroneous code. Neither the code nor the response will be |
114 checked. An example is: |
113 checked. An example is: |
115 |
114 |
116 \begin{center}\small |
115 \begin{center}\small |
117 \begin{tabular}{ll} |
116 \begin{tabular}{ll} |
118 @{text "@{ML_response_fake_both"} & @{text "\"@{cterm \\\"1 + True\\\"}\""}\\ |
117 \<open>@{ML_response_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\ |
119 & @{text "\"Type unification failed \<dots>\"}"} |
118 & \<open>"Type unification failed \<dots>"}\<close> |
120 \end{tabular} |
119 \end{tabular} |
121 \end{center} |
120 \end{center} |
122 |
121 |
123 \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when |
122 \item[$\bullet$] \<open>@{ML_file "name"}\<close> should be used when |
124 referring to a file. It checks whether the file exists. An example |
123 referring to a file. It checks whether the file exists. An example |
125 is |
124 is |
126 |
125 |
127 @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"} |
126 @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"} |
128 \end{itemize} |
127 \end{itemize} |
129 |
128 |
130 The listed antiquotations honour options including @{text "[display]"} and |
129 The listed antiquotations honour options including \<open>[display]\<close> and |
131 @{text "[quotes]"}. For example |
130 \<open>[quotes]\<close>. For example |
132 |
131 |
133 \begin{center}\small |
132 \begin{center}\small |
134 @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} |
133 \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"} |
135 \end{center} |
134 \end{center} |
136 |
135 |
137 whereas |
136 whereas |
138 |
137 |
139 \begin{center}\small |
138 \begin{center}\small |
140 @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} |
139 \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close> |
141 \end{center} |
140 \end{center} |
142 |
141 |
143 \item Functions and value bindings cannot be defined inside antiquotations; they need |
142 \item Functions and value bindings cannot be defined inside antiquotations; they need |
144 to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} |
143 to be included inside \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> |
145 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
144 environments. In this way they are also checked by the compiler. Some \LaTeX-hack in |
146 the tutorial, however, ensures that the environment markers are not printed. |
145 the tutorial, however, ensures that the environment markers are not printed. |
147 |
146 |
148 \item Line numbers can be printed using |
147 \item Line numbers can be printed using |
149 \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"} |
148 \isacommand{ML} \isa{\%linenos}~\<open>\<verbopen> \<dots> \<verbclose>\<close> |
150 for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The |
149 for ML-code or \isacommand{lemma} \isa{\%linenos} \<open>...\<close> for proofs. The |
151 tag is \isa{\%linenosgray} when the numbered text should be gray. |
150 tag is \isa{\%linenosgray} when the numbered text should be gray. |
152 |
151 |
153 \end{itemize} |
152 \end{itemize} |
154 |
153 |
155 *} |
154 \<close> |
156 |
155 |
157 |
156 |
158 |
157 |
159 end |
158 end |