author | wenzelm |
Sun, 10 Oct 2010 19:49:18 +0100 | |
changeset 39835 | 6cefd96bb71d |
parent 39830 | 7c501d7f1e45 |
child 39850 | f4c614ece7ed |
permissions | -rw-r--r-- |
29755 | 1 |
theory "ML" |
2 |
imports Base |
|
3 |
begin |
|
18538 | 4 |
|
39822 | 5 |
chapter {* Isabelle/ML *} |
20489 | 6 |
|
39823 | 7 |
text {* Isabelle/ML is best understood as a certain culture based on |
8 |
Standard ML. Thus it is not a new programming language, but a |
|
9 |
certain way to use SML at an advanced level within the Isabelle |
|
10 |
environment. This covers a variety of aspects that are geared |
|
11 |
towards an efficient and robust platform for applications of formal |
|
12 |
logic with fully foundational proof construction --- according to |
|
13 |
the well-known \emph{LCF principle}. There are specific library |
|
14 |
modules and infrastructure to address the needs for such difficult |
|
15 |
tasks. For example, the raw parallel programming model of Poly/ML |
|
16 |
is presented as considerably more abstract concept of \emph{future |
|
17 |
values}, which is then used to augment the inference kernel, proof |
|
18 |
interpreter, and theory loader accordingly. |
|
19 |
||
20 |
The main aspects of Isabelle/ML are introduced below. These |
|
21 |
first-hand explanations should help to understand how proper |
|
22 |
Isabelle/ML is to be read and written, and to get access to the |
|
23 |
wealth of experience that is expressed in the source text and its |
|
24 |
history of changes.\footnote{See |
|
25 |
\url{http://isabelle.in.tum.de/repos/isabelle} for the full |
|
26 |
Mercurial history. There are symbolic tags to refer to official |
|
27 |
Isabelle releases, as opposed to arbitrary \emph{tip} versions that |
|
28 |
merely reflect snapshots that are never really up-to-date.} *} |
|
29 |
||
30 |
||
31 |
section {* SML embedded into Isabelle/Isar *} |
|
32 |
||
39824 | 33 |
text {* ML and Isar are intertwined via an open-ended bootstrap |
34 |
process that provides more and more programming facilities and |
|
35 |
logical content in an alternating manner. Bootstrapping starts from |
|
36 |
the raw environment of existing implementations of Standard ML |
|
37 |
(mainly Poly/ML, but also SML/NJ). |
|
39823 | 38 |
|
39824 | 39 |
Isabelle/Pure marks the point where the original ML toplevel is |
40 |
superseded by the Isar toplevel that maintains a uniform environment |
|
41 |
for arbitrary ML values (see also \secref{sec:context}). This |
|
42 |
formal context holds logical entities as well as ML compiler |
|
43 |
bindings, among many other things. Raw Standard ML is never |
|
44 |
encountered again after the initial bootstrap of Isabelle/Pure. |
|
39823 | 45 |
|
39824 | 46 |
Object-logics such as Isabelle/HOL are built within the |
47 |
Isabelle/ML/Isar environment of Pure by introducing suitable |
|
48 |
theories with associated ML text, either inlined or as separate |
|
49 |
files. Thus Isabelle/HOL is defined as a regular user-space |
|
50 |
application within the Isabelle framework. Further add-on tools can |
|
51 |
be implemented in ML within the Isar context in the same manner: ML |
|
52 |
is part of the regular user-space repertoire of Isabelle. |
|
39823 | 53 |
*} |
54 |
||
39824 | 55 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
56 |
subsection {* Isar ML commands *} |
39823 | 57 |
|
58 |
text {* The primary Isar source language provides various facilities |
|
59 |
to open a ``window'' to the underlying ML compiler. Especially see |
|
39824 | 60 |
@{command_ref "use"} and @{command_ref "ML"}, which work exactly the |
61 |
same way, only the source text is provided via a file vs.\ inlined, |
|
62 |
respectively. Apart from embedding ML into the main theory |
|
63 |
definition like that, there are many more commands that refer to ML |
|
64 |
source, such as @{command_ref setup} or @{command_ref declaration}. |
|
65 |
An example of even more fine-grained embedding of ML into Isar is |
|
66 |
the proof method @{method_ref tactic}, which refines the pending goal state |
|
67 |
via a given expression of type @{ML_type tactic}. |
|
68 |
*} |
|
39823 | 69 |
|
39824 | 70 |
text %mlex {* The following artificial example demonstrates some ML |
71 |
toplevel declarations within the implicit Isar theory context. This |
|
72 |
is regular functional programming without referring to logical |
|
73 |
entities yet. |
|
39823 | 74 |
*} |
75 |
||
76 |
ML {* |
|
77 |
fun factorial 0 = 1 |
|
78 |
| factorial n = n * factorial (n - 1) |
|
79 |
*} |
|
80 |
||
39824 | 81 |
text {* \noindent Here the ML environment is really managed by |
82 |
Isabelle, i.e.\ the @{ML factorial} function is not yet accessible |
|
83 |
in the preceding paragraph, nor in a different theory that is |
|
84 |
independent from the current one in the import hierarchy. |
|
39823 | 85 |
|
86 |
Removing the above ML declaration from the source text will remove |
|
87 |
any trace of this definition as expected. The Isabelle/ML toplevel |
|
88 |
environment is managed in a \emph{stateless} way: unlike the raw ML |
|
39824 | 89 |
toplevel or similar command loops of Computer Algebra systems, there |
90 |
are no global side-effects involved here.\footnote{Such a stateless |
|
91 |
compilation environment is also a prerequisite for robust parallel |
|
92 |
compilation within independent nodes of the implicit theory |
|
93 |
development graph.} |
|
39823 | 94 |
|
95 |
\bigskip The next example shows how to embed ML into Isar proofs. |
|
39824 | 96 |
Instead of @{command_ref "ML"} for theory mode, we use @{command_ref |
97 |
"ML_prf"} for proof mode. As illustrated below, its effect on the |
|
98 |
ML environment is local to the whole proof body, while ignoring its |
|
99 |
internal block structure. |
|
100 |
*} |
|
39823 | 101 |
|
102 |
example_proof |
|
103 |
ML_prf {* val a = 1 *} |
|
39824 | 104 |
{ -- {* Isar block structure ignored by ML environment *} |
39823 | 105 |
ML_prf {* val b = a + 1 *} |
39824 | 106 |
} -- {* Isar block structure ignored by ML environment *} |
39823 | 107 |
ML_prf {* val c = b + 1 *} |
108 |
qed |
|
109 |
||
39824 | 110 |
text {* \noindent By side-stepping the normal scoping rules for Isar |
111 |
proof blocks, embedded ML code can refer to the different contexts |
|
112 |
explicitly, and manipulate corresponding entities, e.g.\ export a |
|
113 |
fact from a block context. |
|
39823 | 114 |
|
39824 | 115 |
\bigskip Two further ML commands are useful in certain situations: |
116 |
@{command_ref ML_val} and @{command_ref ML_command} are both |
|
117 |
\emph{diagnostic} in the sense that there is no effect on the |
|
118 |
underlying environment, and can thus used anywhere (even outside a |
|
119 |
theory). The examples below produce long strings of digits by |
|
120 |
invoking @{ML factorial}: @{command ML_val} already takes care of |
|
121 |
printing the ML toplevel result, but @{command ML_command} is silent |
|
122 |
so we produce an explicit output message. |
|
123 |
*} |
|
39823 | 124 |
|
125 |
ML_val {* factorial 100 *} |
|
126 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
|
127 |
||
128 |
example_proof |
|
39824 | 129 |
ML_val {* factorial 100 *} (* FIXME check/fix indentation *) |
39823 | 130 |
ML_command {* writeln (string_of_int (factorial 100)) *} |
131 |
qed |
|
132 |
||
133 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
134 |
subsection {* Compile-time context *} |
39823 | 135 |
|
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
136 |
text {* Whenever the ML compiler is invoked within Isabelle/Isar, the |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
137 |
formal context is passed as a thread-local reference variable. Thus |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
138 |
ML code may access the theory context during compilation, by reading |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
139 |
or writing the (local) theory under construction. Note that such |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
140 |
direct access to the compile-time context is rare; in practice it is |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
141 |
typically via some derived ML functions. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
142 |
*} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
143 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
144 |
text %mlref {* |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
145 |
\begin{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
146 |
@{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\ |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
147 |
@{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\ |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
148 |
\end{mldecls} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
149 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
150 |
\begin{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
151 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
152 |
\item @{ML "ML_Context.the_generic_context ()"} refers to the theory |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
153 |
context of the ML toplevel --- at compile time. ML code needs to |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
154 |
take care to refer to @{ML "ML_Context.the_generic_context ()"} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
155 |
correctly. Recall that evaluation of a function body is delayed |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
156 |
until actual run-time. |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
157 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
158 |
\item @{ML "Context.>>"}~@{text f} applies context transformation |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
159 |
@{text f} to the implicit context of the ML toplevel. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
160 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
161 |
\end{description} |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
162 |
|
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
163 |
It is very important to note that the above functions are really |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
164 |
restricted to the compile time, even though the ML compiler is |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
165 |
invoked at run-time. The majority of ML code either uses static |
39825
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
166 |
antiquotations (\secref{sec:ML-antiq}) or refers to the theory or |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
167 |
proof context at run-time, by explicit functional abstraction. |
f9066b94bf07
eliminated fancy \ML logo for the sake of simpler source text (less dependence on LaTeX);
wenzelm
parents:
39824
diff
changeset
|
168 |
*} |
39823 | 169 |
|
170 |
||
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
171 |
subsection {* Antiquotations \label{sec:ML-antiq} *} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
172 |
|
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
173 |
text {* A very important consequence of embedding SML into Isar is the |
39829 | 174 |
concept of \emph{ML antiquotation}. First, the standard token |
175 |
language of ML is augmented by special syntactic entities of the |
|
176 |
following form: |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
177 |
|
39829 | 178 |
\indexouternonterm{antiquote} |
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
179 |
\begin{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
180 |
antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
181 |
; |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
182 |
\end{rail} |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
183 |
|
39829 | 184 |
\noindent Here @{syntax nameref} and @{syntax args} are regular |
185 |
outer syntax categories. Note that attributes and proof methods use |
|
186 |
similar syntax. |
|
39823 | 187 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
188 |
\medskip A regular antiquotation @{text "@{name args}"} processes |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
189 |
its arguments by the usual means of the Isar source language, and |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
190 |
produces corresponding ML source text, either as literal |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
191 |
\emph{inline} text (e.g. @{text "@{term t}"}) or abstract |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
192 |
\emph{value} (e.g. @{text "@{thm th}"}). This pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
193 |
scheme allows to refer to formal entities in a robust manner, with |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
194 |
proper static scoping and with some degree of logical checking of |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
195 |
small portions of the code. |
39823 | 196 |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
197 |
Special antiquotations like @{text "@{let \<dots>}"} or @{text "@{note |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
198 |
\<dots>}"} augment the compilation context without generating code. The |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
199 |
non-ASCII braces @{text "\<lbrace>"} and @{text "\<rbrace>"} allow to delimit the |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
200 |
effect by introducing local blocks within the pre-compilation |
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
201 |
environment. |
39829 | 202 |
|
203 |
\bigskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader |
|
204 |
perspective on Isabelle/ML antiquotations. |
|
205 |
*} |
|
206 |
||
39830 | 207 |
text %mlantiq {* |
39829 | 208 |
\begin{matharray}{rcl} |
209 |
@{ML_antiquotation_def "let"} & : & @{text ML_antiquotation} \\ |
|
210 |
@{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\ |
|
211 |
\end{matharray} |
|
212 |
||
213 |
\begin{rail} |
|
214 |
'let' ((term + 'and') '=' term + 'and') |
|
215 |
; |
|
216 |
||
217 |
'note' (thmdef? thmrefs + 'and') |
|
218 |
; |
|
219 |
\end{rail} |
|
220 |
||
221 |
\begin{description} |
|
222 |
||
223 |
\item @{text "@{let p = t}"} binds schematic variables in the |
|
224 |
pattern @{text "p"} by higher-order matching against the term @{text |
|
225 |
"t"}. This is analogous to the regular @{command_ref let} command |
|
226 |
in the Isar proof language. The pre-compilation environment is |
|
227 |
augmented by auxiliary term bindings, without emitting ML source. |
|
228 |
||
229 |
\item @{text "@{note a = b\<^sub>1 \<dots> b\<^sub>n}"} recalls existing facts @{text |
|
230 |
"b\<^sub>1, \<dots>, b\<^sub>n"}, binding the result as @{text a}. This is analogous to |
|
231 |
the regular @{command_ref note} command in the Isar proof language. |
|
232 |
The pre-compilation environment is augmented by auxiliary fact |
|
233 |
bindings, without emitting ML source. |
|
234 |
||
235 |
\end{description} |
|
236 |
*} |
|
237 |
||
238 |
text %mlex {* The following artificial example gives a first |
|
239 |
impression about using the antiquotation elements introduced so far, |
|
240 |
together with the basic @{text "@{thm}"} antiquotation defined |
|
241 |
later. |
|
242 |
*} |
|
243 |
||
244 |
ML {* |
|
245 |
\<lbrace> |
|
246 |
@{let ?t = my_term} |
|
247 |
@{note my_refl = reflexive [of ?t]} |
|
248 |
fun foo th = Thm.transitive th @{thm my_refl} |
|
249 |
\<rbrace> |
|
250 |
*} |
|
251 |
||
252 |
text {* |
|
253 |
The extra block delimiters do not affect the compiled code itself, i.e.\ |
|
254 |
function @{ML foo} is available in the present context. |
|
39827
d829ce302ca4
basic setup for ML antiquotations -- with rail diagrams;
wenzelm
parents:
39825
diff
changeset
|
255 |
*} |
39823 | 256 |
|
39835 | 257 |
|
258 |
section {* Message output channels *} |
|
259 |
||
260 |
text {* Isabelle provides output channels for different kinds of |
|
261 |
messages: regular output, high-volume tracing information, warnings, |
|
262 |
and errors. |
|
263 |
||
264 |
Depending on the user interface involved, these messages may appear |
|
265 |
in different text styles or colours. The standard output for |
|
266 |
terminal sessions prefixes each line of warnings by @{verbatim |
|
267 |
"###"} and errors by @{verbatim "***"}, but leaves anything else |
|
268 |
unchanged. |
|
269 |
||
270 |
Messages are associated with the transaction context of the running |
|
271 |
Isar command. This enables the front-end to manage commands and |
|
272 |
resulting messages together. For example, after deleting a command |
|
273 |
from a given theory document version, the corresponding message |
|
274 |
output can be retracted from the display. *} |
|
275 |
||
276 |
text %mlref {* |
|
277 |
\begin{mldecls} |
|
278 |
@{index_ML writeln: "string -> unit"} \\ |
|
279 |
@{index_ML tracing: "string -> unit"} \\ |
|
280 |
@{index_ML warning: "string -> unit"} \\ |
|
281 |
@{index_ML error: "string -> 'a"} \\ |
|
282 |
\end{mldecls} |
|
283 |
||
284 |
\begin{description} |
|
285 |
||
286 |
\item @{ML writeln}~@{text "text"} outputs @{text "text"} as regular |
|
287 |
message. This is the primary message output operation of Isabelle |
|
288 |
and should be used by default. |
|
289 |
||
290 |
\item @{ML tracing}~@{text "text"} outputs @{text "text"} as special |
|
291 |
tracing message, indicating potential high-volume output to the |
|
292 |
front-end (hundreds or thousands of messages issued by a single |
|
293 |
command). The idea is to allow the user-interface to downgrade the |
|
294 |
quality of message display to achieve higher throughput. |
|
295 |
||
296 |
Note that the user might have to take special actions to see tracing |
|
297 |
output, e.g.\ switch to a different output window. So this channel |
|
298 |
should not be used for regular output. |
|
299 |
||
300 |
\item @{ML warning}~@{text "text"} outputs @{text "text"} as |
|
301 |
warning, which typically means some extra emphasis on the front-end |
|
302 |
side (color highlighting, icon). |
|
303 |
||
304 |
\item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text |
|
305 |
"text"} and thus lets the Isar toplevel print @{text "text"} on the |
|
306 |
error channel, which typically means some extra emphasis on the |
|
307 |
front-end side (color highlighting, icon). |
|
308 |
||
309 |
This assumes that the exception is not handled before the command |
|
310 |
terminates. Handling exception @{ML ERROR}~@{text "text"} is a |
|
311 |
perfectly legal alternative: it means that the error is absorbed |
|
312 |
without any message output. |
|
313 |
||
314 |
\end{description} |
|
315 |
||
316 |
\begin{warn} |
|
317 |
The actual error channel is accessed via @{ML Output.error_msg}, but |
|
318 |
the interaction protocol of Proof~General \emph{crashes} if that |
|
319 |
function is used in regular ML code: error output and toplevel |
|
320 |
command failure always need to coincide here. |
|
321 |
\end{warn} |
|
322 |
||
323 |
\begin{warn} |
|
324 |
Regular Isabelle/ML code should output messages exclusively by the |
|
325 |
official channels. Using raw I/O on \emph{stdout} or \emph{stderr} |
|
326 |
instead (e.g.\ via @{ML TextIO.output}) is apt to cause problems in |
|
327 |
the presence of parallel and asynchronous processing of Isabelle |
|
328 |
theories. Such raw output might be displayed by the front-end in |
|
329 |
some system console log, with a low chance that the user will ever |
|
330 |
see it. Moreover, as a genuine side-effect on global process |
|
331 |
channels, there is no proper way to retract output when Isar command |
|
332 |
transactions are reset. |
|
333 |
\end{warn} |
|
334 |
*} |
|
335 |
||
30270
61811c9224a6
dummy changes to produce a new changeset of these files;
wenzelm
parents:
29755
diff
changeset
|
336 |
end |