src/Doc/Implementation/Integration.thy

 text {*
   The Isar \emph{toplevel state} represents the outermost configuration that
   is transformed by a sequence of transitions (commands) within a theory body.
   This is a pure value with pure functions acting on it in a timeless and
   stateless manner. Historically, the sequence of transitions was wrapped up
-  as sequential command loop, such that commands are applied sequentially
-  one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
-  usually works in parallel in multi-threaded Isabelle/ML.
+  as sequential command loop, such that commands are applied one-by-one. In
+  contemporary Isabelle/Isar, processing toplevel commands usually works in
+  parallel in multi-threaded Isabelle/ML \cite{Wenzel:2009,Wenzel:2013:ITP}.
 *}
 
 
 subsection {* Toplevel state *}
 

   theory}, or @{text proof}. The initial toplevel is empty; a theory is
   commenced by a @{command theory} header; within a theory we may use theory
   commands such as @{command definition}, or state a @{command theorem} to be
   proven. A proof state accepts a rich collection of Isar proof commands for
   structured proof composition, or unstructured proof scripts. When the proof
-  is concluded we get back to the theory, which is then updated by defining
-  the resulting fact. Further theory declarations or theorem statements with
-  proofs may follow, until we eventually conclude the theory development by
-  issuing @{command end} to get back to the empty toplevel.
+  is concluded we get back to the (local) theory, which is then updated by
+  defining the resulting fact. Further theory declarations or theorem
+  statements with proofs may follow, until we eventually conclude the theory
+  development by issuing @{command end} to get back to the empty toplevel.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML_type Toplevel.state} \\
   @{index_ML_exception Toplevel.UNDEF} \\
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
-  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
 
   \begin{description}
 
   \item Type @{ML_type Toplevel.state} represents Isar toplevel

 
   \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
   toplevel state.
 
   \item @{ML Toplevel.theory_of}~@{text "state"} selects the
-  background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
+  background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF}
   for an empty toplevel state.
 
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
-  state if available, otherwise raises @{ML Toplevel.UNDEF}.
-
-  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
-  information for each Isar command being executed.
-
-  \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
-  low-level profiling of the underlying ML runtime system.  For
-  Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
-  profiling.
+  state if available, otherwise it raises @{ML Toplevel.UNDEF}.
 
   \end{description}
 *}
 
 text %mlantiq {*

 
   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.  This acts like an outer case-expression for various
   alternative state transitions.  For example, \isakeyword{qed} works
-  differently for a local proofs vs.\ the global ending of the main
+  differently for a local proofs vs.\ the global ending of an outermost
   proof.
 
-  Toplevel transitions are composed via transition transformers.
-  Internally, Isar commands are put together from an empty transition
-  extended by name and source position.  It is then left to the
-  individual command parser to turn the given concrete syntax into a
-  suitable transition transformer that adjoins actual operations on a
-  theory or proof state etc.
+  Transitions are composed via transition transformers. Internally, Isar
+  commands are put together from an empty transition extended by name and
+  source position. It is then left to the individual command parser to turn
+  the given concrete syntax into a suitable transition transformer that
+  adjoins actual operations on a theory or proof state.
 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->

   \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
   command, with zero or more result states (represented as a lazy
   list).
 
   \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
-  proof command, that returns the resulting theory, after storing the
-  resulting facts in the context etc.
+  proof command, that returns the resulting theory, after applying the
+  resulting facts to the target context.
 
   \end{description}
 *}
 
 

 *}
 
 text %mlref {*
   \begin{mldecls}
   @{index_ML use_thy: "string -> unit"} \\
-  @{index_ML use_thys: "string list -> unit"} \\
+  @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
   @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
   @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
   \end{mldecls}
 
   \begin{description}
 
   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
-  up-to-date wrt.\ the external file store, reloading outdated ancestors as
-  required.
+  up-to-date wrt.\ the external file store; outdated ancestors are reloaded on
+  demand.
 
   \item @{ML use_thys} is similar to @{ML use_thy}, but handles several
   theories simultaneously. Thus it acts like processing the import header of a
   theory, without performing the merge of the result. By loading a whole
   sub-graph of theories, the intrinsic parallelism can be exploited by the
   system to speedup loading.
 
+  This variant is used by default in @{tool build} \cite{isabelle-sys}.
+
   \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
   presently associated with name @{text A}. Note that the result might be
   outdated wrt.\ the file-system content.
 
   \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
   descendants from the theory database.
 
   \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing
   theory value with the theory loader database and updates source version
-  information according to the current file-system state.
+  information according to the file store.
 
   \end{description}
 *}
 
 end