doc-src/IsarImplementation/Thy/Integration.thy

 
 section {* Isar toplevel \label{sec:isar-toplevel} *}
 
 text {* 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.  We
-  shall even incorporate the existing {\ML} toplevel of the compiler
-  and run-time system (cf.\ \secref{sec:ML-toplevel}).
+  integrated into a single read-eval-print loop of Isar commands,
+  which also incorporates the underlying ML compiler.
 
   Isabelle/Isar departs from the original ``LCF system architecture''
-  where {\ML} was really The Meta Language for defining theories and
-  conducting proofs.  Instead, {\ML} now only serves as the
+  where ML was really The Meta Language for defining theories and
+  conducting proofs.  Instead, ML now only serves as the
   implementation language for the system (and user extensions), while
   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.

   @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML_type Toplevel.state} represents Isar toplevel states,
-  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 Type @{ML_type Toplevel.state} represents Isar toplevel
+  states, 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 @{ML Toplevel.UNDEF} is raised for undefined toplevel
   operations.  Many operations work only partially for certain cases,
   since @{ML_type Toplevel.state} is a sum type.
 

 
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
   \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
-  low-level profiling of the underlying {\ML} runtime system.  For
+  low-level profiling of the underlying ML runtime system.  For
   Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
   profiling.
+
+  \end{description}
+*}
+
+text %mlantiq {*
+  \begin{matharray}{rcl}
+  @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
+  point --- as abstract value.
+
+  This only works for diagnostic ML commands, such as @{command
+  ML_val} or @{command ML_command}.
 
   \end{description}
 *}
 
 

 
   \end{description}
 *}
 
 
-subsection {* Toplevel control *}
-
-text {*
-  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 Proof~General.
-
-  \begin{description}
-
-  \item \isacommand{undo} follows the three-level hierarchy of empty
-  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
-  previous proof context, undo after a proof reverts to the theory
-  before the initial goal statement, undo of a theory command reverts
-  to the previous theory value, undo of a theory header discontinues
-  the current theory development and removes it from the theory
-  database (\secref{sec:theory-database}).
-
-  \item \isacommand{kill} aborts the current level of development:
-  kill in a proof context reverts to the theory before the initial
-  goal statement, kill in a theory context aborts the current theory
-  development, removing it from the database.
-
-  \item \isacommand{exit} drops out of the Isar toplevel into the
-  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
-  toplevel state is preserved and may be continued later.
-
-  \item \isacommand{quit} terminates the Isabelle/Isar process without
-  saving.
-
-  \end{description}
-*}
-
-
-section {* ML toplevel \label{sec:ML-toplevel} *}
-
-text {*
-  The {\ML} toplevel provides a read-compile-eval-print loop for {\ML}
-  values, types, structures, and functors.  {\ML} declarations 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 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 --- while
-  observing the usual linearity restrictions
-  (cf.~\secref{sec:context-theory}).
-*}
-
-text %mlref {*
-  \begin{mldecls}
-  @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
-  @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
-  context of the {\ML} toplevel --- at compile time!  {\ML} code needs
-  to take care to refer to @{ML "ML_Context.the_generic_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 @{ML_type theory_ref} (cf.\ \secref{sec:context-theory}).
-
-  \item @{ML "Context.>>"}~@{text f} applies context transformation
-  @{text f} to the implicit context of the {\ML} toplevel.
-
-  \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 instead.  Thus it
-  may be invoked for an arbitrary context later on, without having to
-  worry about any operational details.
-
-  \bigskip
-
-  \begin{mldecls}
-  @{index_ML Isar.main: "unit -> unit"} \\
-  @{index_ML Isar.loop: "unit -> unit"} \\
-  @{index_ML Isar.state: "unit -> Toplevel.state"} \\
-  @{index_ML Isar.exn: "unit -> (exn * string) option"} \\
-  @{index_ML Isar.goal: "unit ->
-  {context: Proof.context, facts: thm list, goal: thm}"} \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item @{ML "Isar.main ()"} invokes the Isar toplevel from {\ML},
-  initializing an empty toplevel state.
-
-  \item @{ML "Isar.loop ()"} continues the Isar toplevel with the
-  current state, after having dropped out of the Isar toplevel loop.
-
-  \item @{ML "Isar.state ()"} and @{ML "Isar.exn ()"} get current
-  toplevel state and error condition, respectively.  This only works
-  after having dropped out of the Isar toplevel loop.
-
-  \item @{ML "Isar.goal ()"} produces the full Isar goal state,
-  consisting of proof context, facts that have been indicated for
-  immediate use, and the tactical goal according to
-  \secref{sec:tactical-goals}.
-
-  \end{description}
-*}
-
-
 section {* Theory database \label{sec:theory-database} *}
 
 text {*
   The theory database maintains a collection of theories, together
   with some administrative information about their original sources,

   is only a hint to the underlying theory loader.  The internal theory
   name space is flat!
 
   Theory @{text A} is associated with the main theory file @{text
   A}\verb,.thy,, which needs to be accessible through the theory
-  loader path.  Any number of additional {\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 @{text \<USES>}, and loading them consecutively
-  within the theory context.  The system keeps track of incoming {\ML}
+  within the theory context.  The system keeps track of incoming ML
   sources and associates them with the current theory.
 
   The basic internal actions of the theory database are @{text
   "update"} and @{text "remove"}: