1.1 --- a/src/Doc/Implementation/Integration.thy	Thu Jun 19 12:05:10 2014 +0200
     1.2 +++ b/src/Doc/Implementation/Integration.thy	Thu Jun 19 12:33:04 2014 +0200
     1.3 @@ -8,43 +8,30 @@
     1.4  
     1.5  section {* Isar toplevel \label{sec:isar-toplevel} *}
     1.6  
     1.7 -text {* The Isar toplevel may be considered the central hub of the
     1.8 -  Isabelle/Isar system, where all key components and sub-systems are
     1.9 -  integrated into a single read-eval-print loop of Isar commands,
    1.10 -  which also incorporates the underlying ML compiler.
    1.11 +text {*
    1.12 +  The Isar \emph{toplevel state} represents the outermost configuration that
    1.13 +  is transformed by a sequence of transitions (commands) within a theory body.
    1.14 +  This is a pure value with pure functions acting on it in a timeless and
    1.15 +  stateless manner. Historically, the sequence of transitions was wrapped up
    1.16 +  as sequential command loop, such that commands are applied sequentially
    1.17 +  one-by-one. In contemporary Isabelle/Isar, processing toplevel commands
    1.18 +  usually works in parallel in multi-threaded Isabelle/ML.
    1.19 +*}
    1.20  
    1.21 -  Isabelle/Isar departs from the original ``LCF system architecture''
    1.22 -  where ML was really The Meta Language for defining theories and
    1.23 -  conducting proofs.  Instead, ML now only serves as the
    1.24 -  implementation language for the system (and user extensions), while
    1.25 -  the specific Isar toplevel supports the concepts of theory and proof
    1.26 -  development natively.  This includes the graph structure of theories
    1.27 -  and the block structure of proofs, support for unlimited undo,
    1.28 -  facilities for tracing, debugging, timing, profiling etc.
    1.29  
    1.30 -  \medskip The toplevel maintains an implicit state, which is
    1.31 -  transformed by a sequence of transitions -- either interactively or
    1.32 -  in batch-mode.
    1.33 +subsection {* Toplevel state *}
    1.34  
    1.35 -  The toplevel state is a disjoint sum of empty @{text toplevel}, or
    1.36 -  @{text theory}, or @{text proof}.  On entering the main Isar loop we
    1.37 -  start with an empty toplevel.  A theory is commenced by giving a
    1.38 -  @{text \<THEORY>} header; within a theory we may issue theory
    1.39 -  commands such as @{text \<DEFINITION>}, or state a @{text
    1.40 -  \<THEOREM>} to be proven.  Now we are within a proof state, with a
    1.41 -  rich collection of Isar proof commands for structured proof
    1.42 -  composition, or unstructured proof scripts.  When the proof is
    1.43 -  concluded we get back to the theory, which is then updated by
    1.44 -  storing the resulting fact.  Further theory declarations or theorem
    1.45 -  statements with proofs may follow, until we eventually conclude the
    1.46 -  theory development by issuing @{text \<END>}.  The resulting theory
    1.47 -  is then stored within the theory database and we are back to the
    1.48 -  empty toplevel.
    1.49 -
    1.50 -  In addition to these proper state transformations, there are also
    1.51 -  some diagnostic commands for peeking at the toplevel state without
    1.52 -  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
    1.53 -  \isakeyword{print-cases}).
    1.54 +text {*
    1.55 +  The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text
    1.56 +  theory}, or @{text proof}. The initial toplevel is empty; a theory is
    1.57 +  commenced by a @{command theory} header; within a theory we may use theory
    1.58 +  commands such as @{command definition}, or state a @{command theorem} to be
    1.59 +  proven. A proof state accepts a rich collection of Isar proof commands for
    1.60 +  structured proof composition, or unstructured proof scripts. When the proof
    1.61 +  is concluded we get back to the theory, which is then updated by defining
    1.62 +  the resulting fact. Further theory declarations or theorem statements with
    1.63 +  proofs may follow, until we eventually conclude the theory development by
    1.64 +  issuing @{command end} to get back to the empty toplevel.
    1.65  *}
    1.66  
    1.67  text %mlref {*
    1.68 @@ -62,9 +49,7 @@
    1.69  
    1.70    \item Type @{ML_type Toplevel.state} represents Isar toplevel
    1.71    states, which are normally manipulated through the concept of
    1.72 -  toplevel transitions only (\secref{sec:toplevel-transition}).  Also
    1.73 -  note that a raw toplevel state is subject to the same linearity
    1.74 -  restrictions as a theory context (cf.~\secref{sec:context-theory}).
    1.75 +  toplevel transitions only (\secref{sec:toplevel-transition}).
    1.76  
    1.77    \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
    1.78    operations.  Many operations work only partially for certain cases,