10 \item The cookbook can be compiled on the command-line with: |
10 \item The cookbook can be compiled on the command-line with: |
11 |
11 |
12 \begin{center} |
12 \begin{center} |
13 @{text "isabelle make"} |
13 @{text "isabelle make"} |
14 \end{center} |
14 \end{center} |
|
15 |
|
16 You very likely need a recent snapshot of Isabelle in order to compile |
|
17 the cookbook. |
15 |
18 |
16 \item You can include references to other Isabelle manuals using the |
19 \item You can include references to other Isabelle manuals using the |
17 reference names from those manuals. To do this the following |
20 reference names from those manuals. To do this the following |
18 four \LaTeX{} commands are defined: |
21 four \LaTeX{} commands are defined: |
19 |
22 |
45 indicate in which structure or structures the ML-expression should be |
48 indicate in which structure or structures the ML-expression should be |
46 evaluated. Examples are: |
49 evaluated. Examples are: |
47 |
50 |
48 \begin{center}\small |
51 \begin{center}\small |
49 \begin{tabular}{lll} |
52 \begin{tabular}{lll} |
50 @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ |
53 @{text "@{ML \"1 + 3\"}"} & & @{ML "1 + 3"}\\ |
51 @{text "@{ML \"a + b\" for a b}"} & produce & @{ML "a + b" for a b}\\ |
54 @{text "@{ML \"a + b\" for a b}"} & \;\;produce\;\; & @{ML "a + b" for a b}\\ |
52 @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ |
55 @{text "@{ML Ident in OuterLex}"} & & @{ML Ident in OuterLex}\\ |
53 \end{tabular} |
56 \end{tabular} |
54 \end{center} |
57 \end{center} |
55 |
58 |
56 \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to |
59 \item[$\bullet$] @{text "@{ML_response \"expr\" \"pat\"}"} should be used to |
57 display ML-expressions and their response. The first expression is checked |
60 display ML-expressions and their response. The first expression is checked |
58 like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern |
61 like in the antiquotation @{text "@{ML \"expr\"}"}; the second is a pattern |
59 that specifies the result the first expression produces. This pattern can |
62 that specifies the result the first expression produces. This pattern can |
60 contain @{text "\<dots>"} for parts that you like to omit. The response of the |
63 contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the |
61 first expression will be checked against this pattern. Examples are: |
64 first expression will be checked against this pattern. Examples are: |
62 |
65 |
63 \begin{center}\small |
66 \begin{center}\small |
64 \begin{tabular}{l} |
67 \begin{tabular}{l} |
65 @{text "@{ML_response \"1+2\" \"3\"}"}\\ |
68 @{text "@{ML_response \"1+2\" \"3\"}"}\\ |
86 when the result cannot be constructed or the code generates an |
89 when the result cannot be constructed or the code generates an |
87 exception. Examples are: |
90 exception. Examples are: |
88 |
91 |
89 \begin{center}\small |
92 \begin{center}\small |
90 \begin{tabular}{ll} |
93 \begin{tabular}{ll} |
91 @{text "@{ML_response"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ |
94 @{text "@{ML_response_fake"} & @{text "\"cterm_of @{theory} @{term \\\"a + b = c\\\"}\"}"}\\ |
92 & @{text "\"a + b = c\"}"}\smallskip\\ |
95 & @{text "\"a + b = c\"}"}\smallskip\\ |
93 @{text "@{ML_response"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ |
96 @{text "@{ML_response_fake"} & @{text "\"($$ \\\"x\\\") (explode \\\"world\\\")\""}\\ |
94 & @{text "\"Exception FAIL raised\"}"} |
97 & @{text "\"Exception FAIL raised\"}"} |
95 \end{tabular} |
98 \end{tabular} |
96 \end{center} |
99 \end{center} |
97 |
100 |
|
101 which produce respectively |
|
102 |
|
103 \begin{center}\small |
|
104 \begin{tabular}{p{7.2cm}} |
|
105 @{ML_response_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\ |
|
106 @{ML_response_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"} |
|
107 \end{tabular} |
|
108 \end{center} |
98 |
109 |
|
110 This output mimics to some extend what the user sees when running the |
|
111 code. |
|
112 |
99 \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be |
113 \item[$\bullet$] @{text "@{ML_response_fake_both \"expr\" \"pat\"}"} can be |
100 used to show erroneous code. Neither the code nor the response will be |
114 used to show erroneous code. Neither the code nor the response will be |
101 checked. An example is: |
115 checked. An example is: |
102 |
116 |
103 \begin{center}\small |
117 \begin{center}\small |
106 & @{text "\"Type unification failed \<dots>\"}"} |
120 & @{text "\"Type unification failed \<dots>\"}"} |
107 \end{tabular} |
121 \end{tabular} |
108 \end{center} |
122 \end{center} |
109 |
123 |
110 \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when |
124 \item[$\bullet$] @{text "@{ML_file \"name\"}"} should be used when |
111 referring to a file. It checks whether the file exists. |
125 referring to a file. It checks whether the file exists. An example |
|
126 is |
|
127 |
|
128 @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"} |
112 \end{itemize} |
129 \end{itemize} |
113 |
130 |
114 The listed antiquotations honour options including @{text "[display]"} and |
131 The listed antiquotations honour options including @{text "[display]"} and |
115 @{text "[quotes]"}. For example |
132 @{text "[quotes]"}. For example |
116 |
133 |
117 \begin{center}\small |
134 \begin{center}\small |
118 @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} |
135 @{text "@{ML [quotes] \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces\;\; @{text [quotes] "foobar"} |
119 \end{center} |
136 \end{center} |
120 |
137 |
121 while |
138 whereas |
122 |
139 |
123 \begin{center}\small |
140 \begin{center}\small |
124 @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} |
141 @{text "@{ML \"\\\"foo\\\" ^ \\\"bar\\\"\"}"} \;\;produces only\;\; @{text "foobar"} |
125 \end{center} |
142 \end{center} |
126 |
143 |