4 |
4 |
5 chapter {* First Steps *} |
5 chapter {* First Steps *} |
6 |
6 |
7 text {* |
7 text {* |
8 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code |
8 Isabelle programming is done in ML. Just like lemmas and proofs, ML-code |
9 in Isabelle is part of a theory. If you want to follow the code given in |
9 for Isabelle must be part of a theory. If you want to follow the code given in |
10 this chapter, we assume you are working inside the theory starting with |
10 this chapter, we assume you are working inside the theory starting with |
11 |
11 |
12 \begin{quote} |
12 \begin{quote} |
13 \begin{tabular}{@ {}l} |
13 \begin{tabular}{@ {}l} |
14 \isacommand{theory} FirstSteps\\ |
14 \isacommand{theory} FirstSteps\\ |
156 (TextIO.output (stream, (strip_specials s)); |
156 (TextIO.output (stream, (strip_specials s)); |
157 TextIO.output (stream, "\n"); |
157 TextIO.output (stream, "\n"); |
158 TextIO.flushOut stream)) *} |
158 TextIO.flushOut stream)) *} |
159 |
159 |
160 text {* |
160 text {* |
161 Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"} |
161 Calling now |
|
162 |
|
163 @{ML [display,gray] "redirect_tracing (TextIO.openOut \"foo.bar\")"} |
|
164 |
162 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
165 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
163 |
166 |
164 You can print out error messages with the function @{ML [index] error}; for example: |
167 You can print out error messages with the function @{ML [index] error}; for |
|
168 example:\footnote{FIXME: unwanted pagebreak} |
165 |
169 |
166 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
170 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
167 "Exception- ERROR \"foo\" raised |
171 "Exception- ERROR \"foo\" raised |
168 At command \"ML\"."} |
172 At command \"ML\"."} |
169 |
173 |
170 This function raises the exception @{text ERROR} which will then |
174 This function raises the exception @{text ERROR}, which will then |
171 be displayed by the infrastructure. |
175 be displayed by the infrastructure. |
172 |
176 |
173 |
177 |
174 (FIXME Mention how to work with @{ML [index] debug in Toplevel} and |
178 (FIXME Mention how to work with @{ML [index] debug in Toplevel} and |
175 @{ML [index] profiling in Toplevel}.) |
179 @{ML [index] profiling in Toplevel}.) |
191 |
195 |
192 text {* |
196 text {* |
193 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} |
197 Most often you want to inspect data of type @{ML_type term}, @{ML_type cterm} |
194 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing |
198 or @{ML_type thm}. Isabelle contains elaborate pretty-printing functions for printing |
195 them (see Section \ref{sec:pretty}), |
199 them (see Section \ref{sec:pretty}), |
196 but for quick-and-dirty solutions they are far too unwieldy. A simple way to transform |
200 but for quick-and-dirty solutions they are far too unwieldy. One way to transform |
197 a term into a string is to use the function @{ML [index] string_of_term in Syntax}. |
201 a term into a string is to use the function @{ML [index] string_of_term in Syntax}. |
198 |
202 |
199 @{ML_response_fake [display,gray] |
203 @{ML_response_fake [display,gray] |
200 "Syntax.string_of_term @{context} @{term \"1::nat\"}" |
204 "Syntax.string_of_term @{context} @{term \"1::nat\"}" |
201 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} |
205 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""} |
202 |
206 |
203 This produces a string with some additional information encoded in it. The string |
207 This produces a string with some additional information encoded in it. The string |
204 can be properly printed by using the function @{ML [index] writeln}. |
208 can be properly printed by using either the function @{ML [index] writeln} or |
|
209 @{ML [index] tracing}. |
205 |
210 |
206 @{ML_response_fake [display,gray] |
211 @{ML_response_fake [display,gray] |
207 "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})" |
212 "writeln (Syntax.string_of_term @{context} @{term \"1::nat\"})" |
208 "\"1\""} |
213 "\"1\""} |
209 |
214 |
268 |
273 |
269 fun string_of_thms_no_vars ctxt thms = |
274 fun string_of_thms_no_vars ctxt thms = |
270 commas (map (string_of_thm_no_vars ctxt) thms) *} |
275 commas (map (string_of_thm_no_vars ctxt) thms) *} |
271 |
276 |
272 text {* |
277 text {* |
273 When printing out several parcels of information that semantiaclly |
278 When printing out several parcels of information that semantically |
274 belong together, like a warning message consisting of a term and |
279 belong together, like a warning message consisting for example |
275 a type, you should try to keep this information together |
280 of a term and a type, you should try to keep this information |
276 in a single string. So do not print out information as |
281 together in a single string. So do not print out information as |
277 |
282 |
278 @{ML_response_fake [display,gray] |
283 @{ML_response_fake [display,gray] |
279 "tracing \"First half,\"; |
284 "tracing \"First half,\"; |
280 tracing \"and second half.\"" |
285 tracing \"and second half.\"" |
281 "First half, |
286 "First half, |