77 @{ML [display] "warning (makestring 1)"} |
77 @{ML [display] "warning (makestring 1)"} |
78 |
78 |
79 However this only works if the type of what is converted is monomorphic and is not |
79 However this only works if the type of what is converted is monomorphic and is not |
80 a function. |
80 a function. |
81 |
81 |
82 The funtion @{ML "warning"} should only be used for testing purposes, because any |
82 The function @{ML "warning"} should only be used for testing purposes, because any |
83 output this funtion generates will be overwritten as soon as an error is |
83 output this function generates will be overwritten as soon as an error is |
84 raised. For printing anything more serious and elaborate, the |
84 raised. For printing anything more serious and elaborate, the |
85 function @{ML tracing} should be used. This function writes all output into |
85 function @{ML tracing} should be used. This function writes all output into |
86 a separate tracing buffer. For example |
86 a separate tracing buffer. For example |
87 |
87 |
88 @{ML [display] "tracing \"foo\""} |
88 @{ML [display] "tracing \"foo\""} |
89 |
89 |
90 It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is |
90 It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is |
91 printed to a separate file, e.g. to prevent Proof General from choking on massive |
91 printed to a separate file, e.g. to prevent Proof General from choking on massive |
92 amounts of trace output. This rediretion can be achieved using the code |
92 amounts of trace output. This redirection can be achieved using the code |
93 *} |
93 *} |
94 |
94 |
95 ML{* |
95 ML{* |
96 val strip_specials = |
96 val strip_specials = |
97 let |
97 let |
212 \item @{term "{ [x::int] | x. x \<le> -2 }"} |
212 \item @{term "{ [x::int] | x. x \<le> -2 }"} |
213 \end{itemize} |
213 \end{itemize} |
214 |
214 |
215 Hint: The third term is already quite big, and the pretty printer |
215 Hint: The third term is already quite big, and the pretty printer |
216 may omit parts of it by default. If you want to see all of it, you |
216 may omit parts of it by default. If you want to see all of it, you |
217 can use the following ML funtion to set the limit to a value high |
217 can use the following ML function to set the limit to a value high |
218 enough: |
218 enough: |
219 \end{exercise} |
219 \end{exercise} |
220 |
220 |
221 @{ML [display] "print_depth 50"} |
221 @{ML [display] "print_depth 50"} |
222 |
222 |
251 text {* |
251 text {* |
252 |
252 |
253 While antiquotations are very convenient for constructing terms and types, |
253 While antiquotations are very convenient for constructing terms and types, |
254 they can only construct fixed terms. Unfortunately, one often needs to construct terms |
254 they can only construct fixed terms. Unfortunately, one often needs to construct terms |
255 dynamically. For example, a function that returns the implication |
255 dynamically. For example, a function that returns the implication |
256 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the typ @{term "\<tau>"} |
256 @{text "\<And>(x::\<tau>). P x \<Longrightarrow> Q x"} taking @{term P}, @{term Q} and the type @{term "\<tau>"} |
257 as arguments can only be written as |
257 as arguments can only be written as |
258 *} |
258 *} |
259 |
259 |
260 ML {* |
260 ML {* |
261 fun make_imp P Q tau = |
261 fun make_imp P Q tau = |
290 \end{center} |
290 \end{center} |
291 |
291 |
292 The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because |
292 The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because |
293 these constants are defined within type classes; the prefix @{text "HOL"} indicates in |
293 these constants are defined within type classes; the prefix @{text "HOL"} indicates in |
294 which theory they are defined. Guessing such internal names can sometimes be quite hard. |
294 which theory they are defined. Guessing such internal names can sometimes be quite hard. |
295 Therefore Isabellle provides the antiquotation @{text "@{const_name \<dots>}"} which does the |
295 Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the |
296 expansion automatically, for example: |
296 expansion automatically, for example: |
297 |
297 |
298 @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} |
298 @{ML_response_fake [display] "@{const_name \"Nil\"}" "List.list.Nil"} |
299 |
299 |
300 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |
300 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?) |