doc-src/IsarImplementation/Thy/document/integration.tex

 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
 The Isar toplevel may be considered the centeral hub of the
   Isabelle/Isar system, where all key components and sub-systems are
-  integrated into a single read-eval-print loop of Isar commands.
-  Here we even incorporate the existing {\ML} toplevel of the compiler
+  integrated into a single read-eval-print loop of Isar commands.  We
+  shall even incorporate the existing {\ML} toplevel of the compiler
   and run-time system (cf.\ \secref{sec:ML-toplevel}).
 
-  Isabelle/Isar departs from original ``LCF system architecture''
+  Isabelle/Isar departs from the original ``LCF system architecture''
   where {\ML} was really The Meta Language for defining theories and
-  conducting proofs.  Instead, {\ML} merely serves as the
+  conducting proofs.  Instead, {\ML} now only serves as the
   implementation language for the system (and user extensions), while
-  our specific Isar toplevel supports particular notions of
-  incremental theory and proof development more directly.  This
-  includes the graph structure of theories and the block structure of
-  proofs, support for unlimited undo, facilities for tracing,
-  debugging, timing, profiling.
+  the specific Isar toplevel supports the concepts of theory and proof
+  development natively.  This includes the graph structure of theories
+  and the block structure of proofs, support for unlimited undo,
+  facilities for tracing, debugging, timing, profiling etc.
 
   \medskip The toplevel maintains an implicit state, which is
   transformed by a sequence of transitions -- either interactively or
   in batch-mode.  In interactive mode, Isar state transitions are
   encapsulated as safe transactions, such that both failure and undo
   are handled conveniently without destroying the underlying draft
   theory (cf.~\secref{sec:context-theory}).  In batch mode,
-  transitions operate in a strictly linear (destructive) fashion, such
-  that error conditions abort the present attempt to construct a
-  theory altogether.
+  transitions operate in a linear (destructive) fashion, such that
+  error conditions abort the present attempt to construct a theory or
+  proof altogether.
 
   The toplevel state is a disjoint sum of empty \isa{toplevel}, or
   \isa{theory}, or \isa{proof}.  On entering the main Isar loop we
   start with an empty toplevel.  A theory is commenced by giving a
   \isa{{\isasymTHEORY}} header; within a theory we may issue theory

   \end{mldecls}
 
   \begin{description}
 
   \item \verb|Toplevel.state| represents Isar toplevel states,
-  which are normally only manipulated through the toplevel transition
-  concept (\secref{sec:toplevel-transition}).  Also note that a
-  toplevel state is subject to the same linerarity restrictions as a
-  theory context (cf.~\secref{sec:context-theory}).
+  which are normally manipulated through the concept of toplevel
+  transitions only (\secref{sec:toplevel-transition}).  Also note that
+  a raw toplevel state is subject to the same linearity restrictions
+  as a theory context (cf.~\secref{sec:context-theory}).
 
   \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
-  operations: \verb|Toplevel.state| is a sum type, many operations
-  work only partially for certain cases.
-
-  \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
-
-  \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
-  (!), otherwise raises \verb|Toplevel.UNDEF|.
-
-  \item \verb|Toplevel.proof_of| gets the Isar proof state if
-  available, otherwise raises \verb|Toplevel.UNDEF|.
+  operations.  Many operations work only partially for certain cases,
+  since \verb|Toplevel.state| is a sum type.
+
+  \item \verb|Toplevel.is_toplevel|~\isa{state} checks for an empty
+  toplevel state.
+
+  \item \verb|Toplevel.theory_of|~\isa{state} selects the theory of
+  a theory or proof (!), otherwise raises \verb|Toplevel.UNDEF|.
+
+  \item \verb|Toplevel.proof_of|~\isa{state} selects the Isar proof
+  state if available, otherwise raises \verb|Toplevel.UNDEF|.
 
   \item \verb|set Toplevel.debug| makes the toplevel print further
   details about internal error conditions, exceptions being raised
   etc.
 
   \item \verb|set Toplevel.timing| makes the toplevel print timing
   information for each Isar command being executed.
 
-  \item \verb|Toplevel.profiling| controls low-level profiling of the
-  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
-  and 2 space profiling.}
+  \item \verb|Toplevel.profiling|~\verb|:=|~\isa{n} controls
+  low-level profiling of the underlying {\ML} runtime system.  For
+  Poly/ML, \isa{n\ {\isacharequal}\ {\isadigit{1}}} means time and \isa{n\ {\isacharequal}\ {\isadigit{2}}} space
+  profiling.
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 %
 \isadelimmlref
 %
 \endisadelimmlref
 %
-\isamarkupsubsection{Toplevel transitions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-An Isar toplevel transition consists of a partial
-  function on the toplevel state, with additional information for
-  diagnostics and error reporting: there are fields for command name,
-  source position, optional source text, as well as flags for
-  interactive-only commands (which issue a warning in batch-mode),
-  printing of result state, etc.
-
-  The operational part is represented as a sequential union of a list
-  of partial functions, which are tried in turn until the first one
-  succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  For example,
-  a single Isar command like \isacommand{qed} consists of the union of
-  some function \verb|Proof.state -> Proof.state| for proofs
-  within proofs, plus \verb|Proof.state -> theory| for proofs at
-  the outer theory level.
+\isamarkupsubsection{Toplevel transitions \label{sec:toplevel-transition}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An Isar toplevel transition consists of a partial function on the
+  toplevel state, with additional information for diagnostics and
+  error reporting: there are fields for command name, source position,
+  optional source text, as well as flags for interactive-only commands
+  (which issue a warning in batch-mode), printing of result state,
+  etc.
+
+  The operational part is represented as the sequential union of a
+  list of partial functions, which are tried in turn until the first
+  one succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  This acts
+  like an outer case-expression for various alternative state
+  transitions.  For example, \isakeyword{qed} acts differently for a
+  local proofs vs.\ the global ending of the main proof.
 
   Toplevel transitions are composed via transition transformers.
   Internally, Isar commands are put together from an empty transition
   extended by name and source position (and optional source text).  It
   is then left to the individual command parser to turn the given
-  syntax body into a suitable transition transformer that adjoin
+  concrete syntax into a suitable transition transformer that adjoin
   actual operations on a theory or proof state etc.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimmlref

 \verb|  Toplevel.transition -> Toplevel.transition| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|Toplevel.print| sets the print flag, which causes the
-  resulting state of the transition to be echoed in interactive mode.
-
-  \item \verb|Toplevel.no_timing| indicates that the transition should
-  never show timing information, e.g.\ because it is merely a
-  diagnostic command.
-
-  \item \verb|Toplevel.keep| adjoins a diagnostic function.
-
-  \item \verb|Toplevel.theory| adjoins a theory transformer.
-
-  \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
-  which turns a theory into a proof state.  The theory may be changed
-  before entering the proof; the generic Isar goal setup includes an
-  argument that specifies how to apply the proven result to the
-  theory, when the proof is finished.
-
-  \item \verb|Toplevel.proof| adjoins a deterministic proof command,
-  with a singleton result state.
-
-  \item \verb|Toplevel.proofs| adjoins a general proof command, with
-  zero or more result states (represented as a lazy list).
-
-  \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
-  command, that returns the resulting theory, after storing the
-  resulting facts etc.
+  \item \verb|Toplevel.print|~\isa{tr} sets the print flag, which
+  causes the toplevel loop to echo the result state (in interactive
+  mode).
+
+  \item \verb|Toplevel.no_timing|~\isa{tr} indicates that the
+  transition should never show timing information, e.g.\ because it is
+  a diagnostic command.
+
+  \item \verb|Toplevel.keep|~\isa{tr} adjoins a diagnostic
+  function.
+
+  \item \verb|Toplevel.theory|~\isa{tr} adjoins a theory
+  transformer.
+
+  \item \verb|Toplevel.theory_to_proof|~\isa{tr} adjoins a global
+  goal function, which turns a theory into a proof state.  The theory
+  may be changed before entering the proof; the generic Isar goal
+  setup includes an argument that specifies how to apply the proven
+  result to the theory, when the proof is finished.
+
+  \item \verb|Toplevel.proof|~\isa{tr} adjoins a deterministic
+  proof command, with a singleton result.
+
+  \item \verb|Toplevel.proofs|~\isa{tr} adjoins a general proof
+  command, with zero or more result states (represented as a lazy
+  list).
+
+  \item \verb|Toplevel.proof_to_theory|~\isa{tr} adjoins a
+  concluding proof command, that returns the resulting theory, after
+  storing the resulting facts etc.
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 \isamarkupsubsection{Toplevel control%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Apart from regular toplevel transactions there are a few
-  special control commands that modify the behavior the toplevel
-  itself, and only make sense in interactive mode.  Under normal
-  circumstances, the user encounters these only implicitly as part of
-  the protocol between the Isabelle/Isar system and a user-interface
-  such as ProofGeneral.
+There are a few special control commands that modify the behavior
+  the toplevel itself, and only make sense in interactive mode.  Under
+  normal circumstances, the user encounters these only implicitly as
+  part of the protocol between the Isabelle/Isar system and a
+  user-interface such as ProofGeneral.
 
   \begin{description}
 
   \item \isacommand{undo} follows the three-level hierarchy of empty
   toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the

   operate on the global system state, which consists of the compiler
   environment plus the values of {\ML} reference variables.  There is
   no clean way to undo {\ML} declarations, except for reverting to a
   previously saved state of the whole Isabelle process.  {\ML} input
   is either read interactively from a TTY, or from a string (usually
-  within a theory text), or from a source file (usually associated
-  with a theory).
+  within a theory text), or from a source file (usually loaded from a
+  theory).
 
   Whenever the {\ML} toplevel is active, the current Isabelle theory
   context is passed as an internal reference variable.  Thus {\ML}
   code may access the theory context during compilation, it may even
-  change the value of a theory being under construction --- following
-  the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
+  change the value of a theory being under construction --- while
+  observing the usual linearity restrictions
+  (cf.~\secref{sec:context-theory}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
 \isadelimmlref
 %

   when dropping out of the interactive Isar toplevel into {\ML}, or
   when Isar invokes {\ML} to process code from a string or a file.
 
   \item \verb|the_context ()| refers to the theory context of the
   {\ML} toplevel --- at compile time!  {\ML} code needs to take care
-  to refer to \verb|the_context ()| correctly, recall that evaluation
-  of a function body is delayed until actual runtime.  Moreover,
-  persistent {\ML} toplevel bindings to an unfinished theory should be
-  avoided: code should either project out the desired information
-  immediately, or produce an explicit \verb|theory_ref| (cf.\
-  \secref{sec:context-theory}).
+  to refer to \verb|the_context ()| correctly.  Recall that
+  evaluation of a function body is delayed until actual runtime.
+  Moreover, persistent {\ML} toplevel bindings to an unfinished theory
+  should be avoided: code should either project out the desired
+  information immediately, or produce an explicit \verb|theory_ref| (cf.\ \secref{sec:context-theory}).
 
   \item \verb|Context.>>|~\isa{f} applies theory transformation
   \isa{f} to the current theory of the {\ML} toplevel.  In order to
   work as expected, the theory should be still under construction, and
   the Isar language element that invoked the {\ML} compiler in the
-  first place shoule be ready to accept the changed theory value
+  first place should be ready to accept the changed theory value
   (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
-  Otherwise the theory may get destroyed!
+  Otherwise the theory becomes stale!
 
   \end{description}
 
   It is very important to note that the above functions are really
   restricted to the compile time, even though the {\ML} compiler is
   invoked at runtime!  The majority of {\ML} code uses explicit
-  functional arguments of a theory or proof context, as required.
-  Thus it may get run in an arbitrary context later on.
+  functional arguments of a theory or proof context instead.  Thus it
+  may be invoked for an arbitrary context later on, without having to
+  worry about any operational details.
 
   \bigskip
 
   \begin{mldecls}
   \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\

   \end{mldecls}
 
   \begin{description}
 
   \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
-  initializing the state to empty toplevel state.
+  initializing an empty toplevel state.
 
   \item \verb|Isar.loop ()| continues the Isar toplevel with the
-  current state, after dropping out of the Isar toplevel loop.
+  current state, after having dropped out of the Isar toplevel loop.
 
   \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
-  toplevel state and optional error condition, respectively.  This
-  only works after dropping out of the Isar toplevel loop.
-
-  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|.
+  toplevel state and error condition, respectively.  This only works
+  after having dropped out of the Isar toplevel loop.
+
+  \item \verb|Isar.context ()| produces the proof context from \verb|Isar.state ()|, analogous to \verb|Context.proof_of|
+  (\secref{sec:generic-context}).
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 %
 \isadelimmlref
 %
 \endisadelimmlref
 %
-\isamarkupsection{Theory database%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The theory database maintains a collection of theories,
-  together with some administrative information about the original
-  sources, which are held in an external store (i.e.\ a collection of
-  directories within the regular file system of the underlying
-  platform).
-
-  The theory database is organized as a directed acyclic graph, with
-  entries referenced by theory name.  Although some external
-  interfaces allow to include a directory specification, this is only
-  a hint to the underlying theory loader mechanism: the internal
-  theory name space is flat.
+\isamarkupsection{Theory database \label{sec:theory-database}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The theory database maintains a collection of theories, together
+  with some administrative information about their original sources,
+  which are held in an external store (i.e.\ some directory within the
+  regular file system).
+
+  The theory database is organized as a directed acyclic graph;
+  entries are referenced by theory name.  Although some additional
+  interfaces allow to include a directory specification as well, this
+  is only a hint to the underlying theory loader.  The internal theory
+  name space is flat!
 
   Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
-  loader path.  A number of optional {\ML} source files may be
+  loader path.  Any number of additional {\ML} source files may be
   associated with each theory, by declaring these dependencies in the
   theory header as \isa{{\isasymUSES}}, and loading them consecutively
   within the theory context.  The system keeps track of incoming {\ML}
-  sources and associates them with the current theory.  The special
-  theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
-  been concluded, in order to support legacy proof {\ML} proof
-  scripts.
+  sources and associates them with the current theory.  The file
+  \isa{A}\verb,.ML, is loaded after a theory has been concluded, in
+  order to support legacy proof {\ML} proof scripts.
 
   The basic internal actions of the theory database are \isa{update}, \isa{outdate}, and \isa{remove}:
 
   \begin{itemize}
 
   \item \isa{update\ A} introduces a link of \isa{A} with a
   \isa{theory} value of the same name; it asserts that the theory
-  sources are consistent with that value.
+  sources are now consistent with that value;
 
   \item \isa{outdate\ A} invalidates the link of a theory database
-  entry to its sources, but retains the present theory value.
-
-  \item \isa{remove\ A} removes entry \isa{A} from the theory
+  entry to its sources, but retains the present theory value;
+
+  \item \isa{remove\ A} deletes entry \isa{A} from the theory
   database.
   
   \end{itemize}
 
   These actions are propagated to sub- or super-graphs of a theory
-  entry in the usual way, in order to preserve global consistency of
-  the state of all loaded theories with the sources of the external
-  store.  This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
-  all descendants; \isa{remove} will \isa{remove} all
-  descendants.
+  entry as expected, in order to preserve global consistency of the
+  state of all loaded theories with the sources of the external store.
+  This implies certain causalities between actions: \isa{update}
+  or \isa{outdate} of an entry will \isa{outdate} all
+  descendants; \isa{remove} will \isa{remove} all descendants.
 
   \medskip There are separate user-level interfaces to operate on the
   theory database directly or indirectly.  The primitive actions then
   just happen automatically while working with the system.  In
-  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
+  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensures that the
   sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
-  is up-to-date.  Earlier theories are reloaded as required, with
+  is up-to-date, too.  Earlier theories are reloaded as required, with
   \isa{update} actions proceeding in topological order according to
   theory dependencies.  There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
   is achieved eventually.%
 \end{isamarkuptext}%
 \isamarkuptrue%

 \begin{isamarkuptext}%
 \begin{mldecls}
   \indexml{theory}\verb|theory: string -> theory| \\
   \indexml{use-thy}\verb|use_thy: string -> unit| \\
   \indexml{update-thy}\verb|update_thy: string -> unit| \\
-  \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
-  \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
   \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
   \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
   \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
   \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
   \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]

   \end{mldecls}
 
   \begin{description}
 
   \item \verb|theory|~\isa{A} retrieves the theory value presently
-  associated with \isa{A}.  The result is not necessarily
-  up-to-date!
+  associated with name \isa{A}.  Note that the result might be
+  outdated.
 
   \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
   or out-of-date.  It ensures that all parent theories are available
   as well, but does not reload them if older versions are already
   present.
 
   \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
-  the \isa{A} and all of its ancestors are fully up-to-date.
-
-  \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
-  but refrains from loading the attached \isa{A}\verb,.ML, file.
-  This is occasionally useful in replaying legacy {\ML} proof scripts
-  by hand.
-  
-  \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
-  proceeds like \verb|update_thy| for ancestors.
-
-  \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
-  theory \isa{A} and all of its descendants.
-
-  \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
+  theory \isa{A} and all ancestors are fully up-to-date.
+
+  \item \verb|touch_thy|~\isa{A} performs and \isa{outdate} action
+  on theory \isa{A} and all descendants.
+
+  \item \verb|remove_thy|~\isa{A} deletes theory \isa{A} and all
   descendants from the theory database.
 
   \item \verb|ThyInfo.begin_theory| is the basic operation behind a
   \isa{{\isasymTHEORY}} header declaration.  The boolean argument
   indicates the strictness of treating ancestors: for \verb|true| (as
   in interactive mode) like \verb|update_thy|, and for \verb|false| (as
   in batch mode) like \verb|use_thy|.  This is {\ML} functions is
   normally not invoked directly.
 
   \item \verb|ThyInfo.end_theory| concludes the loading of a theory
-  proper; an attached theory {\ML} file may be still loaded later on.
-  This is {\ML} functions is normally not invoked directly.
-
-  \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
-  theory value with the theory loader database.  There is no
-  management of associated sources; this is mainly for bootstrapping.
+  proper.  An attached theory {\ML} file may be still loaded later on.
+  This is function is normally not invoked directly.
+
+  \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
+  existing theory value with the theory loader database.  There is no
+  management of associated sources.
 
   \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
   invoked with the action and theory name being involved; thus derived
   actions may be performed in associated system components, e.g.\
-  maintaining the state of an editor for theory sources.
+  maintaining the state of an editor for the theory sources.
 
   The kind and order of actions occurring in practice depends both on
   user interactions and the internal process of resolving theory
   imports.  Hooks should not rely on a particular policy here!  Any
-  exceptions raised by the hook are ignored by the theory database.
+  exceptions raised by the hook are ignored.
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

 {\isafoldmlref}%
 %
 \isadelimmlref
 %
 \endisadelimmlref
+%
+\isamarkupsection{Sessions and document preparation%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+FIXME%
+\end{isamarkuptext}%
+\isamarkuptrue%
 %
 \isadelimtheory
 %
 \endisadelimtheory
 %