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