equal
deleted
inserted
replaced
193 "if 0=1 then true else (error \"foo\")" |
193 "if 0=1 then true else (error \"foo\")" |
194 "Exception- ERROR \"foo\" raised |
194 "Exception- ERROR \"foo\" raised |
195 At command \"ML\"."} |
195 At command \"ML\"."} |
196 |
196 |
197 This function raises the exception @{text ERROR}, which will then |
197 This function raises the exception @{text ERROR}, which will then |
198 be displayed by the infrastructure. |
198 be displayed by the infrastructure. Note that this exception is meant |
|
199 for ``user-level'' error messages seen by the ``end-user''. |
|
200 |
|
201 For messages where you want to indicate a genuine program error, then |
|
202 use the exception @{text Fail}. Here the infrastructure indicates that this |
|
203 is a low-level exception, and also prints the source position of the ML |
|
204 raise statement. |
199 |
205 |
200 |
206 |
201 \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and |
207 \footnote{\bf FIXME Mention how to work with @{ML_ind debug in Toplevel} and |
202 @{ML_ind profiling in Toplevel}.} |
208 @{ML_ind profiling in Toplevel}.} |
|
209 |
203 *} |
210 *} |
204 |
211 |
205 (* FIXME*) |
212 (* FIXME*) |
206 (* |
213 (* |
207 ML {* reset Toplevel.debug *} |
214 ML {* reset Toplevel.debug *} |
216 |
223 |
217 ML {* Toplevel.program (fn () => innocent ()) *} |
224 ML {* Toplevel.program (fn () => innocent ()) *} |
218 *) |
225 *) |
219 |
226 |
220 text {* |
227 text {* |
|
228 %Kernel exceptions TYPE, TERM, THM also have their place in situations |
|
229 %where kernel-like operations are involved. The printing is similar as for |
|
230 %Fail, although there is some special treatment when Toplevel.debug is |
|
231 %enabled. |
|
232 |
221 Most often you want to inspect data of Isabelle's basic data structures, |
233 Most often you want to inspect data of Isabelle's basic data structures, |
222 namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp} |
234 namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp} |
223 and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions |
235 and @{ML_type thm}. Isabelle contains elaborate pretty-printing functions |
224 for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty |
236 for printing them (see Section \ref{sec:pretty}), but for quick-and-dirty |
225 solutions they are a bit unwieldy. One way to transform a term into a string |
237 solutions they are a bit unwieldy. One way to transform a term into a string |