1.1 --- a/doc-src/IsarImplementation/Thy/document/integration.tex Mon Feb 16 20:25:21 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,521 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{integration}%
1.7 -%
1.8 -\isadelimtheory
1.9 -\isanewline
1.10 -\isanewline
1.11 -\isanewline
1.12 -%
1.13 -\endisadelimtheory
1.14 -%
1.15 -\isatagtheory
1.16 -\isacommand{theory}\isamarkupfalse%
1.17 -\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
1.18 -\endisatagtheory
1.19 -{\isafoldtheory}%
1.20 -%
1.21 -\isadelimtheory
1.22 -%
1.23 -\endisadelimtheory
1.24 -%
1.25 -\isamarkupchapter{System integration%
1.26 -}
1.27 -\isamarkuptrue%
1.28 -%
1.29 -\isamarkupsection{Isar toplevel \label{sec:isar-toplevel}%
1.30 -}
1.31 -\isamarkuptrue%
1.32 -%
1.33 -\begin{isamarkuptext}%
1.34 -The Isar toplevel may be considered the centeral hub of the
1.35 - Isabelle/Isar system, where all key components and sub-systems are
1.36 - integrated into a single read-eval-print loop of Isar commands. We
1.37 - shall even incorporate the existing {\ML} toplevel of the compiler
1.38 - and run-time system (cf.\ \secref{sec:ML-toplevel}).
1.39 -
1.40 - Isabelle/Isar departs from the original ``LCF system architecture''
1.41 - where {\ML} was really The Meta Language for defining theories and
1.42 - conducting proofs. Instead, {\ML} now only serves as the
1.43 - implementation language for the system (and user extensions), while
1.44 - the specific Isar toplevel supports the concepts of theory and proof
1.45 - development natively. This includes the graph structure of theories
1.46 - and the block structure of proofs, support for unlimited undo,
1.47 - facilities for tracing, debugging, timing, profiling etc.
1.48 -
1.49 - \medskip The toplevel maintains an implicit state, which is
1.50 - transformed by a sequence of transitions -- either interactively or
1.51 - in batch-mode. In interactive mode, Isar state transitions are
1.52 - encapsulated as safe transactions, such that both failure and undo
1.53 - are handled conveniently without destroying the underlying draft
1.54 - theory (cf.~\secref{sec:context-theory}). In batch mode,
1.55 - transitions operate in a linear (destructive) fashion, such that
1.56 - error conditions abort the present attempt to construct a theory or
1.57 - proof altogether.
1.58 -
1.59 - The toplevel state is a disjoint sum of empty \isa{toplevel}, or
1.60 - \isa{theory}, or \isa{proof}. On entering the main Isar loop we
1.61 - start with an empty toplevel. A theory is commenced by giving a
1.62 - \isa{{\isasymTHEORY}} header; within a theory we may issue theory
1.63 - commands such as \isa{{\isasymDEFINITION}}, or state a \isa{{\isasymTHEOREM}} to be proven. Now we are within a proof state, with a
1.64 - rich collection of Isar proof commands for structured proof
1.65 - composition, or unstructured proof scripts. When the proof is
1.66 - concluded we get back to the theory, which is then updated by
1.67 - storing the resulting fact. Further theory declarations or theorem
1.68 - statements with proofs may follow, until we eventually conclude the
1.69 - theory development by issuing \isa{{\isasymEND}}. The resulting theory
1.70 - is then stored within the theory database and we are back to the
1.71 - empty toplevel.
1.72 -
1.73 - In addition to these proper state transformations, there are also
1.74 - some diagnostic commands for peeking at the toplevel state without
1.75 - modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
1.76 - \isakeyword{print-cases}).%
1.77 -\end{isamarkuptext}%
1.78 -\isamarkuptrue%
1.79 -%
1.80 -\isadelimmlref
1.81 -%
1.82 -\endisadelimmlref
1.83 -%
1.84 -\isatagmlref
1.85 -%
1.86 -\begin{isamarkuptext}%
1.87 -\begin{mldecls}
1.88 - \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
1.89 - \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
1.90 - \indexml{Toplevel.is\_toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
1.91 - \indexml{Toplevel.theory\_of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
1.92 - \indexml{Toplevel.proof\_of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
1.93 - \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
1.94 - \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
1.95 - \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
1.96 - \end{mldecls}
1.97 -
1.98 - \begin{description}
1.99 -
1.100 - \item \verb|Toplevel.state| represents Isar toplevel states,
1.101 - which are normally manipulated through the concept of toplevel
1.102 - transitions only (\secref{sec:toplevel-transition}). Also note that
1.103 - a raw toplevel state is subject to the same linearity restrictions
1.104 - as a theory context (cf.~\secref{sec:context-theory}).
1.105 -
1.106 - \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
1.107 - operations. Many operations work only partially for certain cases,
1.108 - since \verb|Toplevel.state| is a sum type.
1.109 -
1.110 - \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
1.111 - toplevel state.
1.112 -
1.113 - \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
1.114 - a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
1.115 -
1.116 - \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
1.117 - state if available, otherwise raises \verb|Toplevel.UNDEF|.
1.118 -
1.119 - \item \verb|set Toplevel.debug| makes the toplevel print further
1.120 - details about internal error conditions, exceptions being raised
1.121 - etc.
1.122 -
1.123 - \item \verb|set Toplevel.timing| makes the toplevel print timing
1.124 - information for each Isar command being executed.
1.125 -
1.126 - \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
1.127 - low-level profiling of the underlying {\ML} runtime system. For
1.128 - Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
1.129 - profiling.
1.130 -
1.131 - \end{description}%
1.132 -\end{isamarkuptext}%
1.133 -\isamarkuptrue%
1.134 -%
1.135 -\endisatagmlref
1.136 -{\isafoldmlref}%
1.137 -%
1.138 -\isadelimmlref
1.139 -%
1.140 -\endisadelimmlref
1.141 -%
1.142 -\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
1.143 -}
1.144 -\isamarkuptrue%
1.145 -%
1.146 -\begin{isamarkuptext}%
1.147 -An Isar toplevel transition consists of a partial function on the
1.148 - toplevel state, with additional information for diagnostics and
1.149 - error reporting: there are fields for command name, source position,
1.150 - optional source text, as well as flags for interactive-only commands
1.151 - (which issue a warning in batch-mode), printing of result state,
1.152 - etc.
1.153 -
1.154 - The operational part is represented as the sequential union of a
1.155 - list of partial functions, which are tried in turn until the first
1.156 - one succeeds. This acts like an outer case-expression for various
1.157 - alternative state transitions. For example, \isakeyword{qed} acts
1.158 - differently for a local proofs vs.\ the global ending of the main
1.159 - proof.
1.160 -
1.161 - Toplevel transitions are composed via transition transformers.
1.162 - Internally, Isar commands are put together from an empty transition
1.163 - extended by name and source position (and optional source text). It
1.164 - is then left to the individual command parser to turn the given
1.165 - concrete syntax into a suitable transition transformer that adjoin
1.166 - actual operations on a theory or proof state etc.%
1.167 -\end{isamarkuptext}%
1.168 -\isamarkuptrue%
1.169 -%
1.170 -\isadelimmlref
1.171 -%
1.172 -\endisadelimmlref
1.173 -%
1.174 -\isatagmlref
1.175 -%
1.176 -\begin{isamarkuptext}%
1.177 -\begin{mldecls}
1.178 - \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
1.179 - \indexml{Toplevel.no\_timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
1.180 - \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
1.181 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.182 - \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
1.183 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.184 - \indexml{Toplevel.theory\_to\_proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
1.185 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.186 - \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
1.187 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.188 - \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
1.189 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.190 - \indexml{Toplevel.end\_proof}\verb|Toplevel.end_proof: (bool -> Proof.state -> Proof.context) ->|\isasep\isanewline%
1.191 -\verb| Toplevel.transition -> Toplevel.transition| \\
1.192 - \end{mldecls}
1.193 -
1.194 - \begin{description}
1.195 -
1.196 - \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
1.197 - causes the toplevel loop to echo the result state (in interactive
1.198 - mode).
1.199 -
1.200 - \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
1.201 - transition should never show timing information, e.g.\ because it is
1.202 - a diagnostic command.
1.203 -
1.204 - \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
1.205 - function.
1.206 -
1.207 - \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
1.208 - transformer.
1.209 -
1.210 - \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
1.211 - goal function, which turns a theory into a proof state. The theory
1.212 - may be changed before entering the proof; the generic Isar goal
1.213 - setup includes an argument that specifies how to apply the proven
1.214 - result to the theory, when the proof is finished.
1.215 -
1.216 - \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
1.217 - proof command, with a singleton result.
1.218 -
1.219 - \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
1.220 - command, with zero or more result states (represented as a lazy
1.221 - list).
1.222 -
1.223 - \item \verb|Toplevel.end_proof|~\isa{tr} adjoins a concluding
1.224 - proof command, that returns the resulting theory, after storing the
1.225 - resulting facts in the context etc.
1.226 -
1.227 - \end{description}%
1.228 -\end{isamarkuptext}%
1.229 -\isamarkuptrue%
1.230 -%
1.231 -\endisatagmlref
1.232 -{\isafoldmlref}%
1.233 -%
1.234 -\isadelimmlref
1.235 -%
1.236 -\endisadelimmlref
1.237 -%
1.238 -\isamarkupsubsection{Toplevel control%
1.239 -}
1.240 -\isamarkuptrue%
1.241 -%
1.242 -\begin{isamarkuptext}%
1.243 -There are a few special control commands that modify the behavior
1.244 - the toplevel itself, and only make sense in interactive mode. Under
1.245 - normal circumstances, the user encounters these only implicitly as
1.246 - part of the protocol between the Isabelle/Isar system and a
1.247 - user-interface such as ProofGeneral.
1.248 -
1.249 - \begin{description}
1.250 -
1.251 - \item \isacommand{undo} follows the three-level hierarchy of empty
1.252 - toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
1.253 - previous proof context, undo after a proof reverts to the theory
1.254 - before the initial goal statement, undo of a theory command reverts
1.255 - to the previous theory value, undo of a theory header discontinues
1.256 - the current theory development and removes it from the theory
1.257 - database (\secref{sec:theory-database}).
1.258 -
1.259 - \item \isacommand{kill} aborts the current level of development:
1.260 - kill in a proof context reverts to the theory before the initial
1.261 - goal statement, kill in a theory context aborts the current theory
1.262 - development, removing it from the database.
1.263 -
1.264 - \item \isacommand{exit} drops out of the Isar toplevel into the
1.265 - underlying {\ML} toplevel (\secref{sec:ML-toplevel}). The Isar
1.266 - toplevel state is preserved and may be continued later.
1.267 -
1.268 - \item \isacommand{quit} terminates the Isabelle/Isar process without
1.269 - saving.
1.270 -
1.271 - \end{description}%
1.272 -\end{isamarkuptext}%
1.273 -\isamarkuptrue%
1.274 -%
1.275 -\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
1.276 -}
1.277 -\isamarkuptrue%
1.278 -%
1.279 -\begin{isamarkuptext}%
1.280 -The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
1.281 - values, types, structures, and functors. {\ML} declarations operate
1.282 - on the global system state, which consists of the compiler
1.283 - environment plus the values of {\ML} reference variables. There is
1.284 - no clean way to undo {\ML} declarations, except for reverting to a
1.285 - previously saved state of the whole Isabelle process. {\ML} input
1.286 - is either read interactively from a TTY, or from a string (usually
1.287 - within a theory text), or from a source file (usually loaded from a
1.288 - theory).
1.289 -
1.290 - Whenever the {\ML} toplevel is active, the current Isabelle theory
1.291 - context is passed as an internal reference variable. Thus {\ML}
1.292 - code may access the theory context during compilation, it may even
1.293 - change the value of a theory being under construction --- while
1.294 - observing the usual linearity restrictions
1.295 - (cf.~\secref{sec:context-theory}).%
1.296 -\end{isamarkuptext}%
1.297 -\isamarkuptrue%
1.298 -%
1.299 -\isadelimmlref
1.300 -%
1.301 -\endisadelimmlref
1.302 -%
1.303 -\isatagmlref
1.304 -%
1.305 -\begin{isamarkuptext}%
1.306 -\begin{mldecls}
1.307 - \indexml{the\_context}\verb|the_context: unit -> theory| \\
1.308 - \indexml{Context.$>$$>$ }\verb|Context.>> : (Context.generic -> Context.generic) -> unit| \\
1.309 - \end{mldecls}
1.310 -
1.311 - \begin{description}
1.312 -
1.313 - \item \verb|the_context ()| refers to the theory context of the
1.314 - {\ML} toplevel --- at compile time! {\ML} code needs to take care
1.315 - to refer to \verb|the_context ()| correctly. Recall that
1.316 - evaluation of a function body is delayed until actual runtime.
1.317 - Moreover, persistent {\ML} toplevel bindings to an unfinished theory
1.318 - should be avoided: code should either project out the desired
1.319 - information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
1.320 -
1.321 - \item \verb|Context.>>|~\isa{f} applies context transformation
1.322 - \isa{f} to the implicit context of the {\ML} toplevel.
1.323 -
1.324 - \end{description}
1.325 -
1.326 - It is very important to note that the above functions are really
1.327 - restricted to the compile time, even though the {\ML} compiler is
1.328 - invoked at runtime! The majority of {\ML} code uses explicit
1.329 - functional arguments of a theory or proof context instead. Thus it
1.330 - may be invoked for an arbitrary context later on, without having to
1.331 - worry about any operational details.
1.332 -
1.333 - \bigskip
1.334 -
1.335 - \begin{mldecls}
1.336 - \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
1.337 - \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
1.338 - \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
1.339 - \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
1.340 - \indexml{Isar.context}\verb|Isar.context: unit -> Proof.context| \\
1.341 - \indexml{Isar.goal}\verb|Isar.goal: unit -> thm| \\
1.342 - \end{mldecls}
1.343 -
1.344 - \begin{description}
1.345 -
1.346 - \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
1.347 - initializing an empty toplevel state.
1.348 -
1.349 - \item \verb|Isar.loop ()| continues the Isar toplevel with the
1.350 - current state, after having dropped out of the Isar toplevel loop.
1.351 -
1.352 - \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
1.353 - toplevel state and error condition, respectively. This only works
1.354 - after having dropped out of the Isar toplevel loop.
1.355 -
1.356 - \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
1.357 - (\secref{sec:generic-context}).
1.358 -
1.359 - \item \verb|Isar.goal ()| picks the tactical goal from \verb|Isar.state ()|, represented as a theorem according to
1.360 - \secref{sec:tactical-goals}.
1.361 -
1.362 - \end{description}%
1.363 -\end{isamarkuptext}%
1.364 -\isamarkuptrue%
1.365 -%
1.366 -\endisatagmlref
1.367 -{\isafoldmlref}%
1.368 -%
1.369 -\isadelimmlref
1.370 -%
1.371 -\endisadelimmlref
1.372 -%
1.373 -\isamarkupsection{Theory database \label{sec:theory-database}%
1.374 -}
1.375 -\isamarkuptrue%
1.376 -%
1.377 -\begin{isamarkuptext}%
1.378 -The theory database maintains a collection of theories, together
1.379 - with some administrative information about their original sources,
1.380 - which are held in an external store (i.e.\ some directory within the
1.381 - regular file system).
1.382 -
1.383 - The theory database is organized as a directed acyclic graph;
1.384 - entries are referenced by theory name. Although some additional
1.385 - interfaces allow to include a directory specification as well, this
1.386 - is only a hint to the underlying theory loader. The internal theory
1.387 - name space is flat!
1.388 -
1.389 - Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
1.390 - loader path. Any number of additional {\ML} source files may be
1.391 - associated with each theory, by declaring these dependencies in the
1.392 - theory header as \isa{{\isasymUSES}}, and loading them consecutively
1.393 - within the theory context. The system keeps track of incoming {\ML}
1.394 - sources and associates them with the current theory. The file
1.395 - \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
1.396 - order to support legacy proof {\ML} proof scripts.
1.397 -
1.398 - The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
1.399 -
1.400 - \begin{itemize}
1.401 -
1.402 - \item \isa{update\ A} introduces a link of \isa{A} with a
1.403 - \isa{theory} value of the same name; it asserts that the theory
1.404 - sources are now consistent with that value;
1.405 -
1.406 - \item \isa{outdate\ A} invalidates the link of a theory database
1.407 - entry to its sources, but retains the present theory value;
1.408 -
1.409 - \item \isa{remove\ A} deletes entry \isa{A} from the theory
1.410 - database.
1.411 -
1.412 - \end{itemize}
1.413 -
1.414 - These actions are propagated to sub- or super-graphs of a theory
1.415 - entry as expected, in order to preserve global consistency of the
1.416 - state of all loaded theories with the sources of the external store.
1.417 - This implies certain causalities between actions: \isa{update}
1.418 - or \isa{outdate} of an entry will \isa{outdate} all
1.419 - descendants; \isa{remove} will \isa{remove} all descendants.
1.420 -
1.421 - \medskip There are separate user-level interfaces to operate on the
1.422 - theory database directly or indirectly. The primitive actions then
1.423 - just happen automatically while working with the system. In
1.424 - particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
1.425 - sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
1.426 - is up-to-date, too. Earlier theories are reloaded as required, with
1.427 - \isa{update} actions proceeding in topological order according to
1.428 - theory dependencies. There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
1.429 - is achieved eventually.%
1.430 -\end{isamarkuptext}%
1.431 -\isamarkuptrue%
1.432 -%
1.433 -\isadelimmlref
1.434 -%
1.435 -\endisadelimmlref
1.436 -%
1.437 -\isatagmlref
1.438 -%
1.439 -\begin{isamarkuptext}%
1.440 -\begin{mldecls}
1.441 - \indexml{theory}\verb|theory: string -> theory| \\
1.442 - \indexml{use\_thy}\verb|use_thy: string -> unit| \\
1.443 - \indexml{use\_thys}\verb|use_thys: string list -> unit| \\
1.444 - \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
1.445 - \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
1.446 - \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
1.447 - \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
1.448 - \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
1.449 - \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
1.450 - \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
1.451 - \end{mldecls}
1.452 -
1.453 - \begin{description}
1.454 -
1.455 - \item \verb|theory|~\isa{A} retrieves the theory value presently
1.456 - associated with name \isa{A}. Note that the result might be
1.457 - outdated.
1.458 -
1.459 - \item \verb|use_thy|~\isa{A} ensures that theory \isa{A} is fully
1.460 - up-to-date wrt.\ the external file store, reloading outdated
1.461 - ancestors as required.
1.462 -
1.463 - \item \verb|use_thys| is similar to \verb|use_thy|, but handles
1.464 - several theories simultaneously. Thus it acts like processing the
1.465 - import header of a theory, without performing the merge of the
1.466 - result, though.
1.467 -
1.468 - \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
1.469 - on theory \isa{A} and all descendants.
1.470 -
1.471 - \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
1.472 - descendants from the theory database.
1.473 -
1.474 - \item \verb|ThyInfo.begin_theory| is the basic operation behind a
1.475 - \isa{{\isasymTHEORY}} header declaration. This is {\ML} functions is
1.476 - normally not invoked directly.
1.477 -
1.478 - \item \verb|ThyInfo.end_theory| concludes the loading of a theory
1.479 - proper and stores the result in the theory database.
1.480 -
1.481 - \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
1.482 - existing theory value with the theory loader database. There is no
1.483 - management of associated sources.
1.484 -
1.485 - \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions. The function will be
1.486 - invoked with the action and theory name being involved; thus derived
1.487 - actions may be performed in associated system components, e.g.\
1.488 - maintaining the state of an editor for the theory sources.
1.489 -
1.490 - The kind and order of actions occurring in practice depends both on
1.491 - user interactions and the internal process of resolving theory
1.492 - imports. Hooks should not rely on a particular policy here! Any
1.493 - exceptions raised by the hook are ignored.
1.494 -
1.495 - \end{description}%
1.496 -\end{isamarkuptext}%
1.497 -\isamarkuptrue%
1.498 -%
1.499 -\endisatagmlref
1.500 -{\isafoldmlref}%
1.501 -%
1.502 -\isadelimmlref
1.503 -%
1.504 -\endisadelimmlref
1.505 -%
1.506 -\isadelimtheory
1.507 -%
1.508 -\endisadelimtheory
1.509 -%
1.510 -\isatagtheory
1.511 -\isacommand{end}\isamarkupfalse%
1.512 -%
1.513 -\endisatagtheory
1.514 -{\isafoldtheory}%
1.515 -%
1.516 -\isadelimtheory
1.517 -%
1.518 -\endisadelimtheory
1.519 -\isanewline
1.520 -\end{isabellebody}%
1.521 -%%% Local Variables:
1.522 -%%% mode: latex
1.523 -%%% TeX-master: "root"
1.524 -%%% End: