18537
|
1 |
|
|
2 |
(* $Id$ *)
|
|
3 |
|
|
4 |
theory integration imports base begin
|
|
5 |
|
|
6 |
chapter {* System integration *}
|
|
7 |
|
20447
|
8 |
section {* Isar toplevel \label{sec:isar-toplevel} *}
|
18537
|
9 |
|
|
10 |
text {* The Isar toplevel may be considered the centeral hub of the
|
|
11 |
Isabelle/Isar system, where all key components and sub-systems are
|
20451
|
12 |
integrated into a single read-eval-print loop of Isar commands. We
|
|
13 |
shall even incorporate the existing {\ML} toplevel of the compiler
|
18537
|
14 |
and run-time system (cf.\ \secref{sec:ML-toplevel}).
|
|
15 |
|
20451
|
16 |
Isabelle/Isar departs from the original ``LCF system architecture''
|
18537
|
17 |
where {\ML} was really The Meta Language for defining theories and
|
20451
|
18 |
conducting proofs. Instead, {\ML} now only serves as the
|
18537
|
19 |
implementation language for the system (and user extensions), while
|
20451
|
20 |
the specific Isar toplevel supports the concepts of theory and proof
|
|
21 |
development natively. This includes the graph structure of theories
|
|
22 |
and the block structure of proofs, support for unlimited undo,
|
|
23 |
facilities for tracing, debugging, timing, profiling etc.
|
18537
|
24 |
|
|
25 |
\medskip The toplevel maintains an implicit state, which is
|
|
26 |
transformed by a sequence of transitions -- either interactively or
|
|
27 |
in batch-mode. In interactive mode, Isar state transitions are
|
|
28 |
encapsulated as safe transactions, such that both failure and undo
|
|
29 |
are handled conveniently without destroying the underlying draft
|
|
30 |
theory (cf.~\secref{sec:context-theory}). In batch mode,
|
20451
|
31 |
transitions operate in a linear (destructive) fashion, such that
|
|
32 |
error conditions abort the present attempt to construct a theory or
|
|
33 |
proof altogether.
|
18537
|
34 |
|
|
35 |
The toplevel state is a disjoint sum of empty @{text toplevel}, or
|
|
36 |
@{text theory}, or @{text proof}. On entering the main Isar loop we
|
|
37 |
start with an empty toplevel. A theory is commenced by giving a
|
|
38 |
@{text \<THEORY>} header; within a theory we may issue theory
|
20025
|
39 |
commands such as @{text \<DEFINITION>}, or state a @{text
|
|
40 |
\<THEOREM>} to be proven. Now we are within a proof state, with a
|
|
41 |
rich collection of Isar proof commands for structured proof
|
18537
|
42 |
composition, or unstructured proof scripts. When the proof is
|
|
43 |
concluded we get back to the theory, which is then updated by
|
|
44 |
storing the resulting fact. Further theory declarations or theorem
|
|
45 |
statements with proofs may follow, until we eventually conclude the
|
|
46 |
theory development by issuing @{text \<END>}. The resulting theory
|
|
47 |
is then stored within the theory database and we are back to the
|
|
48 |
empty toplevel.
|
|
49 |
|
|
50 |
In addition to these proper state transformations, there are also
|
|
51 |
some diagnostic commands for peeking at the toplevel state without
|
|
52 |
modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
|
|
53 |
\isakeyword{print-cases}).
|
|
54 |
*}
|
|
55 |
|
|
56 |
text %mlref {*
|
|
57 |
\begin{mldecls}
|
|
58 |
@{index_ML_type Toplevel.state} \\
|
|
59 |
@{index_ML Toplevel.UNDEF: "exn"} \\
|
|
60 |
@{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
|
|
61 |
@{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
|
|
62 |
@{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
|
|
63 |
@{index_ML Toplevel.debug: "bool ref"} \\
|
|
64 |
@{index_ML Toplevel.timing: "bool ref"} \\
|
|
65 |
@{index_ML Toplevel.profiling: "int ref"} \\
|
|
66 |
\end{mldecls}
|
|
67 |
|
|
68 |
\begin{description}
|
|
69 |
|
|
70 |
\item @{ML_type Toplevel.state} represents Isar toplevel states,
|
20451
|
71 |
which are normally manipulated through the concept of toplevel
|
|
72 |
transitions only (\secref{sec:toplevel-transition}). Also note that
|
|
73 |
a raw toplevel state is subject to the same linearity restrictions
|
|
74 |
as a theory context (cf.~\secref{sec:context-theory}).
|
18537
|
75 |
|
|
76 |
\item @{ML Toplevel.UNDEF} is raised for undefined toplevel
|
20451
|
77 |
operations. Many operations work only partially for certain cases,
|
|
78 |
since @{ML_type Toplevel.state} is a sum type.
|
18537
|
79 |
|
20451
|
80 |
\item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
|
|
81 |
toplevel state.
|
18537
|
82 |
|
20451
|
83 |
\item @{ML Toplevel.theory_of}~@{text "state"} selects the theory of
|
|
84 |
a theory or proof (!), otherwise raises @{ML Toplevel.UNDEF}.
|
18537
|
85 |
|
20451
|
86 |
\item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
|
|
87 |
state if available, otherwise raises @{ML Toplevel.UNDEF}.
|
18537
|
88 |
|
|
89 |
\item @{ML "set Toplevel.debug"} makes the toplevel print further
|
|
90 |
details about internal error conditions, exceptions being raised
|
|
91 |
etc.
|
|
92 |
|
|
93 |
\item @{ML "set Toplevel.timing"} makes the toplevel print timing
|
|
94 |
information for each Isar command being executed.
|
|
95 |
|
20451
|
96 |
\item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
|
|
97 |
low-level profiling of the underlying {\ML} runtime system. For
|
|
98 |
Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
|
|
99 |
profiling.
|
18537
|
100 |
|
|
101 |
\end{description}
|
|
102 |
*}
|
|
103 |
|
|
104 |
|
20451
|
105 |
subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
|
18537
|
106 |
|
20451
|
107 |
text {*
|
|
108 |
An Isar toplevel transition consists of a partial function on the
|
|
109 |
toplevel state, with additional information for diagnostics and
|
|
110 |
error reporting: there are fields for command name, source position,
|
|
111 |
optional source text, as well as flags for interactive-only commands
|
|
112 |
(which issue a warning in batch-mode), printing of result state,
|
|
113 |
etc.
|
18537
|
114 |
|
20451
|
115 |
The operational part is represented as the sequential union of a
|
|
116 |
list of partial functions, which are tried in turn until the first
|
20475
|
117 |
one succeeds. This acts like an outer case-expression for various
|
|
118 |
alternative state transitions. For example, \isakeyword{qed} acts
|
|
119 |
differently for a local proofs vs.\ the global ending of the main
|
|
120 |
proof.
|
18537
|
121 |
|
|
122 |
Toplevel transitions are composed via transition transformers.
|
|
123 |
Internally, Isar commands are put together from an empty transition
|
|
124 |
extended by name and source position (and optional source text). It
|
|
125 |
is then left to the individual command parser to turn the given
|
20451
|
126 |
concrete syntax into a suitable transition transformer that adjoin
|
18537
|
127 |
actual operations on a theory or proof state etc.
|
|
128 |
*}
|
|
129 |
|
|
130 |
text %mlref {*
|
|
131 |
\begin{mldecls}
|
|
132 |
@{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
|
|
133 |
@{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
|
|
134 |
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
|
|
135 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
136 |
@{index_ML Toplevel.theory: "(theory -> theory) ->
|
|
137 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
138 |
@{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
|
|
139 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
140 |
@{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
|
|
141 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
142 |
@{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
|
|
143 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
144 |
@{index_ML Toplevel.proof_to_theory: "(Proof.state -> theory) ->
|
|
145 |
Toplevel.transition -> Toplevel.transition"} \\
|
|
146 |
\end{mldecls}
|
|
147 |
|
|
148 |
\begin{description}
|
|
149 |
|
20451
|
150 |
\item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
|
|
151 |
causes the toplevel loop to echo the result state (in interactive
|
|
152 |
mode).
|
18537
|
153 |
|
20451
|
154 |
\item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
|
|
155 |
transition should never show timing information, e.g.\ because it is
|
|
156 |
a diagnostic command.
|
18537
|
157 |
|
20451
|
158 |
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
|
|
159 |
function.
|
18537
|
160 |
|
20451
|
161 |
\item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
|
|
162 |
transformer.
|
18537
|
163 |
|
20451
|
164 |
\item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
|
|
165 |
goal function, which turns a theory into a proof state. The theory
|
|
166 |
may be changed before entering the proof; the generic Isar goal
|
|
167 |
setup includes an argument that specifies how to apply the proven
|
|
168 |
result to the theory, when the proof is finished.
|
18558
|
169 |
|
20451
|
170 |
\item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
|
|
171 |
proof command, with a singleton result.
|
18537
|
172 |
|
20451
|
173 |
\item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
|
|
174 |
command, with zero or more result states (represented as a lazy
|
|
175 |
list).
|
18537
|
176 |
|
20451
|
177 |
\item @{ML Toplevel.proof_to_theory}~@{text "tr"} adjoins a
|
|
178 |
concluding proof command, that returns the resulting theory, after
|
|
179 |
storing the resulting facts etc.
|
18537
|
180 |
|
|
181 |
\end{description}
|
|
182 |
*}
|
|
183 |
|
|
184 |
|
|
185 |
subsection {* Toplevel control *}
|
|
186 |
|
20451
|
187 |
text {*
|
|
188 |
There are a few special control commands that modify the behavior
|
|
189 |
the toplevel itself, and only make sense in interactive mode. Under
|
|
190 |
normal circumstances, the user encounters these only implicitly as
|
|
191 |
part of the protocol between the Isabelle/Isar system and a
|
|
192 |
user-interface such as ProofGeneral.
|
18537
|
193 |
|
|
194 |
\begin{description}
|
|
195 |
|
|
196 |
\item \isacommand{undo} follows the three-level hierarchy of empty
|
|
197 |
toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
|
|
198 |
previous proof context, undo after a proof reverts to the theory
|
|
199 |
before the initial goal statement, undo of a theory command reverts
|
|
200 |
to the previous theory value, undo of a theory header discontinues
|
|
201 |
the current theory development and removes it from the theory
|
|
202 |
database (\secref{sec:theory-database}).
|
|
203 |
|
|
204 |
\item \isacommand{kill} aborts the current level of development:
|
|
205 |
kill in a proof context reverts to the theory before the initial
|
|
206 |
goal statement, kill in a theory context aborts the current theory
|
|
207 |
development, removing it from the database.
|
|
208 |
|
|
209 |
\item \isacommand{exit} drops out of the Isar toplevel into the
|
|
210 |
underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
|
|
211 |
toplevel state is preserved and may be continued later.
|
|
212 |
|
|
213 |
\item \isacommand{quit} terminates the Isabelle/Isar process without
|
|
214 |
saving.
|
|
215 |
|
|
216 |
\end{description}
|
|
217 |
*}
|
|
218 |
|
|
219 |
|
|
220 |
section {* ML toplevel \label{sec:ML-toplevel} *}
|
|
221 |
|
20475
|
222 |
text {*
|
|
223 |
The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
|
|
224 |
values, types, structures, and functors. {\ML} declarations operate
|
|
225 |
on the global system state, which consists of the compiler
|
18537
|
226 |
environment plus the values of {\ML} reference variables. There is
|
|
227 |
no clean way to undo {\ML} declarations, except for reverting to a
|
|
228 |
previously saved state of the whole Isabelle process. {\ML} input
|
|
229 |
is either read interactively from a TTY, or from a string (usually
|
20451
|
230 |
within a theory text), or from a source file (usually loaded from a
|
|
231 |
theory).
|
18537
|
232 |
|
|
233 |
Whenever the {\ML} toplevel is active, the current Isabelle theory
|
|
234 |
context is passed as an internal reference variable. Thus {\ML}
|
|
235 |
code may access the theory context during compilation, it may even
|
20451
|
236 |
change the value of a theory being under construction --- while
|
|
237 |
observing the usual linearity restrictions
|
|
238 |
(cf.~\secref{sec:context-theory}).
|
18537
|
239 |
*}
|
|
240 |
|
|
241 |
text %mlref {*
|
|
242 |
\begin{mldecls}
|
|
243 |
@{index_ML context: "theory -> unit"} \\
|
|
244 |
@{index_ML the_context: "unit -> theory"} \\
|
|
245 |
@{index_ML "Context.>> ": "(theory -> theory) -> unit"} \\
|
|
246 |
\end{mldecls}
|
|
247 |
|
|
248 |
\begin{description}
|
|
249 |
|
|
250 |
\item @{ML context}~@{text thy} sets the {\ML} theory context to
|
|
251 |
@{text thy}. This is usually performed automatically by the system,
|
|
252 |
when dropping out of the interactive Isar toplevel into {\ML}, or
|
|
253 |
when Isar invokes {\ML} to process code from a string or a file.
|
|
254 |
|
|
255 |
\item @{ML "the_context ()"} refers to the theory context of the
|
|
256 |
{\ML} toplevel --- at compile time! {\ML} code needs to take care
|
20451
|
257 |
to refer to @{ML "the_context ()"} correctly. Recall that
|
|
258 |
evaluation of a function body is delayed until actual runtime.
|
|
259 |
Moreover, persistent {\ML} toplevel bindings to an unfinished theory
|
|
260 |
should be avoided: code should either project out the desired
|
|
261 |
information immediately, or produce an explicit @{ML_type
|
|
262 |
theory_ref} (cf.\ \secref{sec:context-theory}).
|
18537
|
263 |
|
|
264 |
\item @{ML "Context.>>"}~@{text f} applies theory transformation
|
|
265 |
@{text f} to the current theory of the {\ML} toplevel. In order to
|
|
266 |
work as expected, the theory should be still under construction, and
|
|
267 |
the Isar language element that invoked the {\ML} compiler in the
|
20451
|
268 |
first place should be ready to accept the changed theory value
|
18537
|
269 |
(e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
|
20451
|
270 |
Otherwise the theory becomes stale!
|
18537
|
271 |
|
|
272 |
\end{description}
|
|
273 |
|
|
274 |
It is very important to note that the above functions are really
|
|
275 |
restricted to the compile time, even though the {\ML} compiler is
|
|
276 |
invoked at runtime! The majority of {\ML} code uses explicit
|
20451
|
277 |
functional arguments of a theory or proof context instead. Thus it
|
|
278 |
may be invoked for an arbitrary context later on, without having to
|
|
279 |
worry about any operational details.
|
18537
|
280 |
|
|
281 |
\bigskip
|
|
282 |
|
|
283 |
\begin{mldecls}
|
|
284 |
@{index_ML Isar.main: "unit -> unit"} \\
|
|
285 |
@{index_ML Isar.loop: "unit -> unit"} \\
|
|
286 |
@{index_ML Isar.state: "unit -> Toplevel.state"} \\
|
20025
|
287 |
@{index_ML Isar.context: "unit -> Proof.context"} \\
|
18537
|
288 |
@{index_ML Isar.exn: "unit -> (exn * string) option"} \\
|
|
289 |
\end{mldecls}
|
|
290 |
|
|
291 |
\begin{description}
|
|
292 |
|
|
293 |
\item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
|
20451
|
294 |
initializing an empty toplevel state.
|
18537
|
295 |
|
|
296 |
\item @{ML "Isar.loop ()"} continues the Isar toplevel with the
|
20451
|
297 |
current state, after having dropped out of the Isar toplevel loop.
|
18537
|
298 |
|
|
299 |
\item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
|
20451
|
300 |
toplevel state and error condition, respectively. This only works
|
|
301 |
after having dropped out of the Isar toplevel loop.
|
18537
|
302 |
|
20025
|
303 |
\item @{ML "Isar.context ()"} produces the proof context from @{ML
|
20451
|
304 |
"Isar.state ()"}, analogous to @{ML Context.proof_of}
|
|
305 |
(\secref{sec:generic-context}).
|
20025
|
306 |
|
18537
|
307 |
\end{description}
|
|
308 |
*}
|
|
309 |
|
|
310 |
|
20451
|
311 |
section {* Theory database \label{sec:theory-database} *}
|
18537
|
312 |
|
20451
|
313 |
text {*
|
|
314 |
The theory database maintains a collection of theories, together
|
|
315 |
with some administrative information about their original sources,
|
|
316 |
which are held in an external store (i.e.\ some directory within the
|
|
317 |
regular file system).
|
18537
|
318 |
|
20451
|
319 |
The theory database is organized as a directed acyclic graph;
|
|
320 |
entries are referenced by theory name. Although some additional
|
|
321 |
interfaces allow to include a directory specification as well, this
|
|
322 |
is only a hint to the underlying theory loader. The internal theory
|
|
323 |
name space is flat!
|
18537
|
324 |
|
|
325 |
Theory @{text A} is associated with the main theory file @{text
|
|
326 |
A}\verb,.thy,, which needs to be accessible through the theory
|
20451
|
327 |
loader path. Any number of additional {\ML} source files may be
|
18537
|
328 |
associated with each theory, by declaring these dependencies in the
|
|
329 |
theory header as @{text \<USES>}, and loading them consecutively
|
|
330 |
within the theory context. The system keeps track of incoming {\ML}
|
20451
|
331 |
sources and associates them with the current theory. The file
|
|
332 |
@{text A}\verb,.ML, is loaded after a theory has been concluded, in
|
|
333 |
order to support legacy proof {\ML} proof scripts.
|
18537
|
334 |
|
|
335 |
The basic internal actions of the theory database are @{text
|
18554
|
336 |
"update"}, @{text "outdate"}, and @{text "remove"}:
|
18537
|
337 |
|
|
338 |
\begin{itemize}
|
|
339 |
|
|
340 |
\item @{text "update A"} introduces a link of @{text "A"} with a
|
|
341 |
@{text "theory"} value of the same name; it asserts that the theory
|
20451
|
342 |
sources are now consistent with that value;
|
18537
|
343 |
|
|
344 |
\item @{text "outdate A"} invalidates the link of a theory database
|
20451
|
345 |
entry to its sources, but retains the present theory value;
|
18537
|
346 |
|
20451
|
347 |
\item @{text "remove A"} deletes entry @{text "A"} from the theory
|
18537
|
348 |
database.
|
|
349 |
|
|
350 |
\end{itemize}
|
|
351 |
|
|
352 |
These actions are propagated to sub- or super-graphs of a theory
|
20451
|
353 |
entry as expected, in order to preserve global consistency of the
|
|
354 |
state of all loaded theories with the sources of the external store.
|
|
355 |
This implies certain causalities between actions: @{text "update"}
|
|
356 |
or @{text "outdate"} of an entry will @{text "outdate"} all
|
|
357 |
descendants; @{text "remove"} will @{text "remove"} all descendants.
|
18537
|
358 |
|
|
359 |
\medskip There are separate user-level interfaces to operate on the
|
|
360 |
theory database directly or indirectly. The primitive actions then
|
|
361 |
just happen automatically while working with the system. In
|
|
362 |
particular, processing a theory header @{text "\<THEORY> A
|
20451
|
363 |
\<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
|
18537
|
364 |
sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
|
20451
|
365 |
is up-to-date, too. Earlier theories are reloaded as required, with
|
18537
|
366 |
@{text update} actions proceeding in topological order according to
|
|
367 |
theory dependencies. There may be also a wave of implied @{text
|
|
368 |
outdate} actions for derived theory nodes until a stable situation
|
|
369 |
is achieved eventually.
|
|
370 |
*}
|
|
371 |
|
|
372 |
text %mlref {*
|
|
373 |
\begin{mldecls}
|
|
374 |
@{index_ML theory: "string -> theory"} \\
|
|
375 |
@{index_ML use_thy: "string -> unit"} \\
|
|
376 |
@{index_ML update_thy: "string -> unit"} \\
|
|
377 |
@{index_ML touch_thy: "string -> unit"} \\
|
|
378 |
@{index_ML remove_thy: "string -> unit"} \\[1ex]
|
|
379 |
@{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
|
|
380 |
@{index_ML ThyInfo.end_theory: "theory -> theory"} \\
|
|
381 |
@{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
|
|
382 |
@{verbatim "datatype action = Update | Outdate | Remove"} \\
|
|
383 |
@{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
|
|
384 |
\end{mldecls}
|
|
385 |
|
|
386 |
\begin{description}
|
|
387 |
|
|
388 |
\item @{ML theory}~@{text A} retrieves the theory value presently
|
20451
|
389 |
associated with name @{text A}. Note that the result might be
|
|
390 |
outdated.
|
18537
|
391 |
|
|
392 |
\item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
|
|
393 |
or out-of-date. It ensures that all parent theories are available
|
|
394 |
as well, but does not reload them if older versions are already
|
|
395 |
present.
|
|
396 |
|
|
397 |
\item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
|
20451
|
398 |
theory @{text A} and all ancestors are fully up-to-date.
|
18537
|
399 |
|
20451
|
400 |
\item @{ML touch_thy}~@{text A} performs and @{text outdate} action
|
|
401 |
on theory @{text A} and all descendants.
|
18537
|
402 |
|
20451
|
403 |
\item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
|
18537
|
404 |
descendants from the theory database.
|
|
405 |
|
|
406 |
\item @{ML ThyInfo.begin_theory} is the basic operation behind a
|
|
407 |
@{text \<THEORY>} header declaration. The boolean argument
|
|
408 |
indicates the strictness of treating ancestors: for @{ML true} (as
|
|
409 |
in interactive mode) like @{ML update_thy}, and for @{ML false} (as
|
|
410 |
in batch mode) like @{ML use_thy}. This is {\ML} functions is
|
|
411 |
normally not invoked directly.
|
|
412 |
|
|
413 |
\item @{ML ThyInfo.end_theory} concludes the loading of a theory
|
20451
|
414 |
proper. An attached theory {\ML} file may be still loaded later on.
|
|
415 |
This is function is normally not invoked directly.
|
18537
|
416 |
|
20451
|
417 |
\item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
|
|
418 |
existing theory value with the theory loader database. There is no
|
|
419 |
management of associated sources.
|
18537
|
420 |
|
|
421 |
\item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
|
|
422 |
f} as a hook for theory database actions. The function will be
|
|
423 |
invoked with the action and theory name being involved; thus derived
|
|
424 |
actions may be performed in associated system components, e.g.\
|
20451
|
425 |
maintaining the state of an editor for the theory sources.
|
18537
|
426 |
|
|
427 |
The kind and order of actions occurring in practice depends both on
|
|
428 |
user interactions and the internal process of resolving theory
|
|
429 |
imports. Hooks should not rely on a particular policy here! Any
|
20451
|
430 |
exceptions raised by the hook are ignored.
|
18537
|
431 |
|
|
432 |
\end{description}
|
|
433 |
*}
|
|
434 |
|
|
435 |
end
|