
diff -r a16b18fd6299 -r 6a3f7941c3a0 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Oct 22 20:51:45 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Fri Oct 22 20:57:33 2010 +0100
@@ -18,252 +18,2165 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Advanced ML programming%
+\isamarkupchapter{Isabelle/ML%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/ML is best understood as a certain culture based on
+  Standard ML.  Thus it is not a new programming language, but a
+  certain way to use SML at an advanced level within the Isabelle
+  environment.  This covers a variety of aspects that are geared
+  towards an efficient and robust platform for applications of formal
+  logic with fully foundational proof construction --- according to
+  the well-known \emph{LCF principle}.  There are specific library
+  modules and infrastructure to address the needs for such difficult
+  tasks.  For example, the raw parallel programming model of Poly/ML
+  is presented as considerably more abstract concept of \emph{future
+  values}, which is then used to augment the inference kernel, proof
+  interpreter, and theory loader accordingly.
+
+  The main aspects of Isabelle/ML are introduced below.  These
+  first-hand explanations should help to understand how proper
+  Isabelle/ML is to be read and written, and to get access to the
+  wealth of experience that is expressed in the source text and its
+  history of changes.\footnote{See
+  \url{http://isabelle.in.tum.de/repos/isabelle} for the full
+  Mercurial history.  There are symbolic tags to refer to official
+  Isabelle releases, as opposed to arbitrary \emph{tip} versions that
+  merely reflect snapshots that are never really up-to-date.}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Style and orthography%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The sources of Isabelle/Isar are optimized for
+  \emph{readability} and \emph{maintainability}.  The main purpose is
+  to tell an informed reader what is really going on and how things
+  really work.  This is a non-trivial aim, but it is supported by a
+  certain style of writing Isabelle/ML that has emerged from long
+  years of system development.\footnote{See also the interesting style
+  guide for OCaml
+  \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}
+  which shares many of our means and ends.}
+
+  The main principle behind any coding style is \emph{consistency}.
+  For a single author of a small program this merely means ``choose
+  your style and stick to it''.  A complex project like Isabelle, with
+  long years of development and different contributors, requires more
+  standardization.  A coding style that is changed every few years or
+  with every new contributor is no style at all, because consistency
+  is quickly lost.  Global consistency is hard to achieve, though.
+  One should always strife at least for local consistency of modules
+  and sub-systems, without deviating from some general principles how
+  to write Isabelle/ML.
+
+  In a sense, a common coding style is like an \emph{orthography} for
+  the sources: it helps to read quickly over the text and see through
+  the main points, without getting distracted by accidental
+  presentation of free-style source.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Header and sectioning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle source files have a certain standardized header
+  format (with precise spacing) that follows ancient traditions
+  reaching back to the earliest versions of the system by Larry
+  Paulson.  E.g.\ see \hyperlink{file.~~/src/Pure/thm.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}thm{\isachardot}ML}}}}.
+
+  The header includes at least \verb|Title| and \verb|Author| entries, followed by a prose description of the purpose of
+  the module.  The latter can range from a single line to several
+  paragraphs of explanations.
+
+  The rest of the file is divided into sections, subsections,
+  subsubsections, paragraphs etc.\ using some a layout via ML comments
+  as follows.
+
+\begin{verbatim}
+(*** section ***)
+
+(** subsection **)
+
+(* subsubsection *)
+
+(*short paragraph*)
+
+(*
+  long paragraph
+  more text
+*)
+\end{verbatim}
+
+  As in regular typography, there is some extra space \emph{before}
+  section headings that are adjacent to plain text (not other headings
+  as in the example above).
+
+  \medskip The precise wording of the prose text given in these
+  headings is chosen carefully to indicate the main theme of the
+  subsequent formal ML text.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Naming conventions%
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Style%
+\begin{isamarkuptext}%
+Since ML is the primary medium to express the meaning of the
+  source text, naming of ML entities requires special care.
+
+  \paragraph{Notation.}  A name consists of 1--3 \emph{words} (rarely
+  4, but not more) that are separated by underscore.  There are three
+  variants concerning upper or lower case letters, which are just for
+  certain ML categories as follows:
+
+  \medskip
+  \begin{tabular}{lll}
+  variant & example & ML categories \\\hline
+  lower-case & \verb|foo_bar| & values, types, record fields \\
+  capitalized & \verb|Foo_Bar| & datatype constructors, \\
+    & & structures, functors \\
+  upper-case & \verb|FOO_BAR| & special values (combinators), \\
+    & & exception constructors, signatures \\
+  \end{tabular}
+  \medskip
+
+  For historical reasons, many capitalized names omit underscores,
+  e.g.\ old-style \verb|FooBar| instead of \verb|Foo_Bar|.
+  Genuine mixed-case names are \emph{not} used --- clear division of
+  words is essential for readability.\footnote{Camel-case was invented
+  to workaround the lack of underscore in some early non-ASCII
+  character sets and keywords.  Later it became a habitual in some
+  language communities that are now strong in numbers.}
+
+  A single (capital) character does not count as ``word'' in this
+  respect: some Isabelle/ML are suffixed by extra markers like this:
+  \verb|foo_barT|.
+
+  Name variants are produced by adding 1--3 primes, e.g.\ \verb|foo'|, \verb|foo''|, or \verb|foo'''|, but not \verb|foo''''| or more.  Decimal digits scale better to larger numbers,
+  e.g.\ \verb|foo0|, \verb|foo1|, \verb|foo42|.
+
+  \paragraph{Scopes.}  Apart from very basic library modules, ML
+  structures are not ``opened'', but names are referenced with
+  explicit qualification, as in \verb|Syntax.string_of_term| for
+  example.  When devising names for structures and their components it
+  is important aim at eye-catching compositions of both parts, because
+  this is how they are always seen in the sources and documentation.
+  For the same reasons, aliases of well-known library functions should
+  be avoided.
+
+  Local names of function abstraction or case/lets bindings are
+  typically shorter, sometimes using only rudiments of ``words'',
+  while still avoiding cryptic shorthands.  An auxiliary function
+  called \verb|helper|, \verb|aux|, or \verb|f| is
+  considered bad style.
+
+  Example:
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  fun print_foo ctxt foo =
+    let
+      fun print t = ... Syntax.string_of_term ctxt t ...
+    in ... end;
+
+
+  (* RIGHT *)
+
+  fun print_foo ctxt foo =
+    let
+      val string_of_term = Syntax.string_of_term ctxt;
+      fun print t = ... string_of_term t ...
+    in ... end;
+
+
+  (* WRONG *)
+
+  val string_of_term = Syntax.string_of_term;
+
+  fun print_foo ctxt foo =
+    let
+      fun aux t = ... string_of_term ctxt t ...
+    in ... end;
+
+  \end{verbatim}
+
+
+  \paragraph{Specific conventions.} Here are some important specific
+  name forms that occur frequently in the sources.
+
+  \begin{itemize}
+
+  \item A function that maps \verb|foo| to \verb|bar| is
+  called \verb|foo_to_bar| or \verb|bar_of_foo| (never
+  \verb|foo2bar|, \verb|bar_from_foo|, \verb|bar_for_foo|, or \verb|bar4foo|).
+
+  \item The name component \verb|legacy| means that the operation
+  is about to be discontinued soon.
+
+  \item The name component \verb|old| means that this is historic
+  material that might disappear at some later stage.
+
+  \item The name component \verb|global| means that this works
+  with the background theory instead of the regular local context
+  (\secref{sec:context}), sometimes for historical reasons, sometimes
+  due a genuine lack of locality of the concept involved, sometimes as
+  a fall-back for the lack of a proper context in the application
+  code.  Whenever there is a non-global variant available, the
+  application should be migrated to use it with a proper local
+  context.
+
+  \item Variables of the main context types of the Isabelle/Isar
+  framework (\secref{sec:context} and \chref{ch:local-theory}) have
+  firm naming conventions to allow to visualize the their data flow
+  via plain regular expressions in the editor.  In particular:
+
+  \begin{itemize}
+
+  \item theories are called \verb|thy|, rarely \verb|theory|
+  (never \verb|thry|)
+
+  \item proof contexts are called \verb|ctxt|, rarely \verb|context| (never \verb|ctx|)
+
+  \item generic contexts are called \verb|context|, rarely
+  \verb|ctxt|
+
+  \item local theories are called \verb|lthy|, unless there is an
+  implicit conversion to a general proof context (semantic super-type)
+
+  \end{itemize}
+
+  Variations with primed or decimal numbers are always possible, as
+  well as ``sematic prefixes'' like \verb|foo_thy| or \verb|bar_ctxt|, but the base conventions above need to be preserved.
+
+  \item The main logical entities (\secref{ch:logic}) also have
+  established naming convention:
+
+  \begin{itemize}
+
+  \item sorts are called \verb|S|
+
+  \item types are called \verb|T|, \verb|U|, or \verb|ty| (never \verb|t|)
+
+  \item terms are called \verb|t|, \verb|u|, or \verb|tm| (never \verb|trm|)
+
+  \item certified types are called \verb|cT|, rarely \verb|T|, with variants as for types
+
+  \item certified terms are called \verb|ct|, rarely \verb|t|, with variants as for terms
+
+  \item theorems are called \verb|th|, or \verb|thm|
+
+  \end{itemize}
+
+  Proper semantic names override these conventions completely.  For
+  example, the left-hand side of an equation (as a term) can be called
+  \verb|lhs| (not \verb|lhs_tm|).  Or a term that is treated
+  specifically as a variable can be called \verb|v| or \verb|x|.
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{General source layout%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Like any style guide, also this one should not be interpreted dogmatically, but
-  with care and discernment.  It consists of a collection of
-  recommendations which have been turned out useful over long years of
-  Isabelle system development and are supposed to support writing of readable
-  and managable code.  Special cases encourage derivations,
-  as far as you know what you are doing.
-  \footnote{This style guide is loosely based on
-  \url{http://caml.inria.fr/resources/doc/guides/guidelines.en.html}}
+The general Isabelle/ML source layout imitates regular
+  type-setting to some extent, augmented by the requirements for
+  deeply nested expressions that are commonplace in functional
+  programming.
+
+  \paragraph{Line length} is 80 characters according to ancient
+  standards, but we allow as much as 100 characters, not
+  more.\footnote{Readability requires to keep the beginning of a line
+  in view while watching its end.  Modern wide-screen displays do not
+  change the way how the human brain works.  As a rule of thumb,
+  sources need to be printable on plain paper.} The extra 20
+  characters acknowledge the space requirements due to qualified
+  library references in Isabelle/ML.
+
+  \paragraph{White-space} is used to emphasize the structure of
+  expressions, following mostly standard conventions for mathematical
+  typesetting, as can be seen in plain {\TeX} or {\LaTeX}.  This
+  defines positioning of spaces for parentheses, punctuation, and
+  infixes as illustrated here:
+
+  \begin{verbatim}
+  val x = y + z * (a + b);
+  val pair = (a, b);
+  val record = {foo = 1, bar = 2};
+  \end{verbatim}
+
+  Lines are normally broken \emph{after} an infix operator or
+  punctuation character.  For example:
+
+  \begin{verbatim}
+  val x =
+    a +
+    b +
+    c;
+
+  val tuple =
+   (a,
+    b,
+    c);
+  \end{verbatim}
+
+  Some special infixes (e.g.\ \verb||\verb,|,\verb|>|) work better at the
+  start of the line, but punctuation is always at the end.
+
+  Function application follows the tradition of \isa{{\isasymlambda}}-calculus,
+  not informal mathematics.  For example: \verb|f a b| for a
+  curried function, or \verb|g (a, b)| for a tupled function.
+  Note that the space between \verb|g| and the pair \verb|(a, b)| follows the important principle of
+  \emph{compositionality}: the layout of \verb|g p| does not
+  change when \verb|p| is refined to a concrete pair.
+
+  \paragraph{Indentation} uses plain spaces, never hard
+  tabulators.\footnote{Tabulators were invented to move the carriage
+  of a type-writer to certain predefined positions.  In software they
+  could be used as a primitive run-length compression of consecutive
+  spaces, but the precise result would depend on non-standardized
+  editor configuration.}
+
+  Each level of nesting is indented by 2 spaces, sometimes 1, very
+  rarely 4, never 8.
+
+  Indentation follows a simple logical format that only depends on the
+  nesting depth, not the accidental length of the text that initiates
+  a level of nesting.  Example:
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  if b then
+    expr1_part1
+    expr1_part2
+  else
+    expr2_part1
+    expr2_part2
+
+
+  (* WRONG *)
+
+  if b then expr1_part1
+            expr1_part2
+  else expr2_part1
+       expr2_part2
+  \end{verbatim}
+
+  The second form has many problems: it assumes a fixed-width font
+  when viewing the sources, it uses more space on the line and thus
+  makes it hard to observe its strict length limit (working against
+  \emph{readability}), it requires extra editing to adapt the layout
+  to changes of the initial text (working against
+  \emph{maintainability}) etc.
+
+  \medskip For similar reasons, any kind of two-dimensional or tabular
+  layouts, ASCII-art with lines or boxes of stars etc. should be
+  avoided.
+
+  \paragraph{Complex expressions} consisting of multi-clausal function
+  definitions, \verb|case|, \verb|handle|, \verb|let|,
+  or combinations require special attention.  The syntax of Standard
+  ML is a bit too ambitious in admitting too much variance that can
+  distort the meaning of the text.
+
+  Clauses of \verb|fun|, \verb|fn|, \verb|case|,
+  \verb|handle| get extra indentation to indicate the nesting
+  clearly.  For example:
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  fun foo p1 =
+        expr1
+    | foo p2 =
+        expr2
+
+
+  (* WRONG *)
+
+  fun foo p1 =
+    expr1
+    | foo p2 =
+    expr2
+  \end{verbatim}
+
+  Body expressions consisting of \verb|case| or \verb|let|
+  require care to maintain compositionality, to prevent loss of
+  logical indentation where it is particularly imporant to see the
+  structure of the text later on.  Example:
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  fun foo p1 =
+        (case e of
+          q1 => ...
+        | q2 => ...)
+    | foo p2 =
+        let
+          ...
+        in
+          ...
+        end
+
+
+  (* WRONG *)
+
+  fun foo p1 = case e of
+      q1 => ...
+    | q2 => ...
+    | foo p2 =
+    let
+      ...
+    in
+      ...
+    end
+  \end{verbatim}
+
+  Extra parentheses around \verb|case| expressions are optional,
+  but help to analyse the nesting easily based on simple string
+  matching in the editor.
+
+  \medskip There are two main exceptions to the overall principle of
+  compositionality in the layout of complex expressions.
+
+  \begin{enumerate}
+
+  \item \verb|if| expressions are iterated as if there would be
+  a multi-branch conditional in SML, e.g.
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  if b1 then e1
+  else if b2 then e2
+  else e3
+  \end{verbatim}
+
+  \item \verb|fn| abstractions are often layed-out as if they
+  would lack any structure by themselves.  This traditional form is
+  motivated by the possibility to shift function arguments back and
+  forth wrt.\ additional combinators.  For example:
+
+  \begin{verbatim}
+  (* RIGHT *)
+
+  fun foo x y = fold (fn z =>
+    expr)
+  \end{verbatim}
+
+  Here the visual appearance is that of three arguments \verb|x|,
+  \verb|y|, \verb|z|.
+
+  \end{enumerate}
+
+  Such weakly structured layout should be use with great care.  Here
+  is a counter-example involving \verb|let| expressions:
+
+  \begin{verbatim}
+  (* WRONG *)
+
+  fun foo x = let
+      val y = ...
+    in ... end
+
+  fun foo x =
+  let
+    val y = ...
+  in ... end
+  \end{verbatim}
+
+  \medskip In general the source layout is meant to emphasize the
+  structure of complex language expressions, not to pretend that SML
+  had a completely different syntax (say that of Haskell or Java).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{SML embedded into Isabelle/Isar%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+ML and Isar are intertwined via an open-ended bootstrap
+  process that provides more and more programming facilities and
+  logical content in an alternating manner.  Bootstrapping starts from
+  the raw environment of existing implementations of Standard ML
+  (mainly Poly/ML, but also SML/NJ).
+
+  Isabelle/Pure marks the point where the original ML toplevel is
+  superseded by the Isar toplevel that maintains a uniform environment
+  for arbitrary ML values (see also \secref{sec:context}).  This
+  formal context holds logical entities as well as ML compiler
+  bindings, among many other things.  Raw Standard ML is never
+  encountered again after the initial bootstrap of Isabelle/Pure.
+
+  Object-logics such as Isabelle/HOL are built within the
+  Isabelle/ML/Isar environment of Pure by introducing suitable
+  theories with associated ML text, either inlined or as separate
+  files.  Thus Isabelle/HOL is defined as a regular user-space
+  application within the Isabelle framework.  Further add-on tools can
+  be implemented in ML within the Isar context in the same manner: ML
+  is part of the regular user-space repertoire of Isabelle.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Isar ML commands%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The primary Isar source language provides various facilities
+  to open a ``window'' to the underlying ML compiler.  Especially see
+  \indexref{}{command}{use}\hyperlink{command.use}{\mbox{\isa{\isacommand{use}}}} and \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}}, which work exactly the
+  same way, only the source text is provided via a file vs.\ inlined,
+  respectively.  Apart from embedding ML into the main theory
+  definition like that, there are many more commands that refer to ML
+  source, such as \indexref{}{command}{setup}\hyperlink{command.setup}{\mbox{\isa{\isacommand{setup}}}} or \indexref{}{command}{declaration}\hyperlink{command.declaration}{\mbox{\isa{\isacommand{declaration}}}}.
+  An example of even more fine-grained embedding of ML into Isar is
+  the proof method \indexref{}{method}{tactic}\hyperlink{method.tactic}{\mbox{\isa{tactic}}}, which refines the pending goal state
+  via a given expression of type \verb|tactic|.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example demonstrates some ML
+  toplevel declarations within the implicit Isar theory context.  This
+  is regular functional programming without referring to logical
+  entities yet.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ factorial\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}\isanewline
+\ \ \ \ {\isacharbar}\ factorial\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ factorial\ {\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Here the ML environment is really managed by Isabelle, i.e.\
+  the \verb|factorial| function is not yet accessible in the preceding
+  paragraph, nor in a different theory that is independent from the
+  current one in the import hierarchy.
+
+  Removing the above ML declaration from the source text will remove
+  any trace of this definition as expected.  The Isabelle/ML toplevel
+  environment is managed in a \emph{stateless} way: unlike the raw ML
+  toplevel or similar command loops of Computer Algebra systems, there
+  are no global side-effects involved here.\footnote{Such a stateless
+  compilation environment is also a prerequisite for robust parallel
+  compilation within independent nodes of the implicit theory
+  development graph.}
+
+  \medskip The next example shows how to embed ML into Isar proofs.
+  Instead of \indexref{}{command}{ML}\hyperlink{command.ML}{\mbox{\isa{\isacommand{ML}}}} for theory mode, we use \indexref{}{command}{ML\_prf}\hyperlink{command.ML-prf}{\mbox{\isa{\isacommand{ML{\isacharunderscore}prf}}}} for proof mode.  As illustrated below, its effect on the
+  ML environment is local to the whole proof body, while ignoring its
+  internal block structure.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ a\ {\isacharequal}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ b\ {\isacharequal}\ a\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\ \ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ %
+\isamarkupcmt{Isar block structure ignored by ML environment%
+}
+\isanewline
+\ \ \isacommand{ML{\isacharunderscore}prf}\isamarkupfalse%
+\ {\isacharverbatimopen}\ val\ c\ {\isacharequal}\ b\ {\isacharplus}\ {\isadigit{1}}\ {\isacharverbatimclose}\isanewline
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+By side-stepping the normal scoping rules for Isar proof
+  blocks, embedded ML code can refer to the different contexts
+  explicitly, and manipulate corresponding entities, e.g.\ export a
+  fact from a block context.
+
+  \medskip Two further ML commands are useful in certain situations:
+  \indexref{}{command}{ML\_val}\hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} and \indexref{}{command}{ML\_command}\hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} are both
+  \emph{diagnostic} in the sense that there is no effect on the
+  underlying environment, and can thus used anywhere (even outside a
+  theory).  The examples below produce long strings of digits by
+  invoking \verb|factorial|: \hyperlink{command.ML-val}{\mbox{\isa{\isacommand{ML{\isacharunderscore}val}}}} already takes care of
+  printing the ML toplevel result, but \hyperlink{command.ML-command}{\mbox{\isa{\isacommand{ML{\isacharunderscore}command}}}} is silent
+  so we produce an explicit output message.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\isanewline
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+\isanewline
+\isanewline
+\isacommand{example{\isacharunderscore}proof}\isamarkupfalse%
+\isanewline
+%
+\isadelimML
+\ \ %
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}val}\isamarkupfalse%
+\ {\isacharverbatimopen}\ factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}\ {\isacharverbatimclose}\ \ \isanewline
+\ \ \isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\ writeln\ {\isacharparenleft}string{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}factorial\ {\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+\isanewline
+%
+\endisadelimML
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Compile-time context%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Whenever the ML compiler is invoked within Isabelle/Isar, the
+  formal context is passed as a thread-local reference variable.  Thus
+  ML code may access the theory context during compilation, by reading
+  or writing the (local) theory under construction.  Note that such
+  direct access to the compile-time context is rare; in practice it is
+  typically via some derived ML functions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{ML\_Context.the\_generic\_context}\verb|ML_Context.the_generic_context: unit -> Context.generic| \\
+  \indexdef{}{ML}{Context.$>$$>$}\verb|Context.>>  : (Context.generic -> Context.generic) -> unit| \\
+  \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
+  \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
+  \end{mldecls}
 
   \begin{description}
 
-    \item[fundamental law of programming]
-      Whenever writing code, keep in mind: A program is
-      written once, modified ten times, and read
-      hundred times.  So simplify its writing,
-      always keep future modifications in mind,
-      and never jeopardize readability.  Every second you hesitate
-      to spend on making your code more clear you will
-      have to spend ten times understanding what you have
-      written later on.
+  \item \verb|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 \verb|ML_Context.the_generic_context ()|
+  correctly.  Recall that evaluation of a function body is delayed
+  until actual run-time.
+
+  \item \verb|Context.>>|~\isa{f} applies context transformation
+  \isa{f} to the implicit context of the ML toplevel.
 
-    \item[white space matters]
-      Treat white space in your code as if it determines
-      the meaning of code.
+  \item \verb|bind_thms|~\isa{{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}} stores a list of
+  theorems produced in ML both in the (global) theory context and the
+  ML toplevel, associating it with the provided name.  Theorems are
+  put into a global ``standard'' format before being stored.
 
-      \begin{itemize}
+  \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
+  singleton theorem.
+
+  \end{description}
 
-        \item The space bar is the easiest key to find on the keyboard,
-          press it as often as necessary. \verb|2 + 2| is better
-          than \verb|2+2|, likewise \verb|f (x, y)| is
-          better than \verb|f(x,y)|.
+  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 run-time.  The majority of ML code either uses static
+  antiquotations (\secref{sec:ML-antiq}) or refers to the theory or
+  proof context at run-time, by explicit functional abstraction.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Antiquotations \label{sec:ML-antiq}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A very important consequence of embedding SML into Isar is the
+  concept of \emph{ML antiquotation}.  First, the standard token
+  language of ML is augmented by special syntactic entities of the
+  following form:
 
-        \item Restrict your lines to 80 characters.  This will allow
-          you to keep the beginning of a line in view while watching
-          its end.\footnote{To acknowledge the lax practice of
-          text editing these days, we tolerate as much as 100
-          characters per line, but anything beyond 120 is not
-          considered proper source text.}
-
-        \item Ban tabulators; they are a context-sensitive formatting
-          feature and likely to confuse anyone not using your favorite
-          editor.\footnote{Some modern programming language even
-          forbid tabulators altogether according to the formal syntax
-          definition.}
-
-        \item Get rid of trailing whitespace.  Instead, do not
-          suppress a trailing newline at the end of your files.
+  \indexouternonterm{antiquote}
+  \begin{rail}
+  antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
+  ;
+  \end{rail}
 
-        \item Choose a generally accepted style of indentation,
-          then use it systematically throughout the whole
-          application.  An indentation of two spaces is appropriate.
-          Avoid dangling indentation.
-
-      \end{itemize}
+  Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
+  categories.  Note that attributes and proof methods use similar
+  syntax.
 
-    \item[cut-and-paste succeeds over copy-and-paste]
-       \emph{Never} copy-and-paste code when programming.  If you
-        need the same piece of code twice, introduce a
-        reasonable auxiliary function (if there is no
-        such function, very likely you got something wrong).
-        Any copy-and-paste will turn out to be painful 
-        when something has to be changed later on.
+  \medskip A regular antiquotation \isa{{\isacharat}{\isacharbraceleft}name\ args{\isacharbraceright}} processes
+  its arguments by the usual means of the Isar source language, and
+  produces corresponding ML source text, either as literal
+  \emph{inline} text (e.g. \isa{{\isacharat}{\isacharbraceleft}term\ t{\isacharbraceright}}) or abstract
+  \emph{value} (e.g. \isa{{\isacharat}{\isacharbraceleft}thm\ th{\isacharbraceright}}).  This pre-compilation
+  scheme allows to refer to formal entities in a robust manner, with
+  proper static scoping and with some degree of logical checking of
+  small portions of the code.
 
-    \item[comments]
-      are a device which requires careful thinking before using
-      it.  The best comment for your code should be the code itself.
-      Prefer efforts to write clear, understandable code
-      over efforts to explain nasty code.
+  Special antiquotations like \isa{{\isacharat}{\isacharbraceleft}let\ {\isasymdots}{\isacharbraceright}} or \isa{{\isacharat}{\isacharbraceleft}note\ {\isasymdots}{\isacharbraceright}} augment the compilation context without generating code.  The
+  non-ASCII braces \isa{{\isasymlbrace}} and \isa{{\isasymrbrace}} allow to delimit the
+  effect by introducing local blocks within the pre-compilation
+  environment.
 
-    \item[functional programming is based on functions]
-      Model things as abstract as appropriate.  Avoid unnecessarrily
-      concrete datatype  representations.  For example, consider a function
-      taking some table data structure as argument and performing
-      lookups on it.  Instead of taking a table, it could likewise
-      take just a lookup function.  Accustom
-      your way of coding to the level of expressiveness a functional
-      programming language is giving onto you.
+  \medskip See also \cite{Wenzel-Chaieb:2007b} for a slightly broader
+  perspective on Isabelle/ML antiquotations.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+  \indexdef{}{ML antiquotation}{let}\hypertarget{ML antiquotation.let}{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+  \indexdef{}{ML antiquotation}{note}\hypertarget{ML antiquotation.note}{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+  \end{matharray}
 
-    \item[tuples]
-      are often in the way.  When there is no striking argument
-      to tuple function arguments, just write your function curried.
+  \begin{rail}
+  'let' ((term + 'and') '=' term + 'and')
+  ;
+
+  'note' (thmdef? thmrefs + 'and')
+  ;
+  \end{rail}
+
+  \begin{description}
 
-    \item[telling names]
-      Any name should tell its purpose as exactly as possible, while
-      keeping its length to the absolutely necessary minimum.  Always
-      give the same name to function arguments which have the same
-      meaning. Separate words by underscores (\verb|int_of_string|, not \verb|intOfString|).\footnote{Some
-      recent tools for Emacs include special precautions to cope with
-      bumpy names in \isa{camelCase}, e.g.\ for improved on-screen
-      readability.  It is easier to abstain from using such names in the
-      first place.}
+  \item \isa{{\isacharat}{\isacharbraceleft}let\ p\ {\isacharequal}\ t{\isacharbraceright}} binds schematic variables in the
+  pattern \isa{p} by higher-order matching against the term \isa{t}.  This is analogous to the regular \indexref{}{command}{let}\hyperlink{command.let}{\mbox{\isa{\isacommand{let}}}} command
+  in the Isar proof language.  The pre-compilation environment is
+  augmented by auxiliary term bindings, without emitting ML source.
+
+  \item \isa{{\isacharat}{\isacharbraceleft}note\ a\ {\isacharequal}\ b\isactrlsub {\isadigit{1}}\ {\isasymdots}\ b\isactrlsub n{\isacharbraceright}} recalls existing facts \isa{b\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ b\isactrlsub n}, binding the result as \isa{a}.  This is analogous to
+  the regular \indexref{}{command}{note}\hyperlink{command.note}{\mbox{\isa{\isacommand{note}}}} command in the Isar proof language.
+  The pre-compilation environment is augmented by auxiliary fact
+  bindings, without emitting ML source.
 
   \end{description}%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Thread-safe programming%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following artificial example gives a first
+  impression about using the antiquotation elements introduced so far,
+  together with the basic \isa{{\isacharat}{\isacharbraceleft}thm{\isacharbraceright}} antiquotation defined
+  later.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ {\isaantiqopen}\isanewline
+\ \ \ \ %
+\isaantiq
+let\ {\isacharquery}t\ {\isacharequal}\ my{\isacharunderscore}term%
+\endisaantiq
+\isanewline
+\ \ \ \ %
+\isaantiq
+note\ my{\isacharunderscore}refl\ {\isacharequal}\ reflexive\ {\isacharbrackleft}of\ {\isacharquery}t{\isacharbrackright}%
+\endisaantiq
+\isanewline
+\ \ \ \ fun\ foo\ th\ {\isacharequal}\ Thm{\isachardot}transitive\ th\ %
+\isaantiq
+thm\ my{\isacharunderscore}refl%
+\endisaantiq
+\isanewline
+\ \ {\isaantiqclose}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The extra block delimiters do not affect the compiled code itself, i.e.\
+  function \verb|foo| is available in the present context.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Canonical argument order \label{sec:canonical-argument-order}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Standard ML is a language in the tradition of \isa{{\isasymlambda}}-calculus and \emph{higher-order functional programming},
+  similar to OCaml, Haskell, or Isabelle/Pure and HOL as logical
+  languages.  Getting acquainted with the native style of representing
+  functions in that setting can save a lot of extra boiler-plate of
+  redundant shuffling of arguments, auxiliary abstractions etc.
+
+  First of all, functions are usually \emph{curried}: the idea of
+  \isa{f} taking \isa{n} arguments of type \isa{{\isasymtau}\isactrlsub i} (for
+  \isa{i\ {\isasymin}\ {\isacharbraceleft}{\isadigit{1}}{\isacharcomma}\ {\isasymdots}\ n{\isacharbraceright}}) with result \isa{{\isasymtau}} is represented by
+  the iterated function space \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymdots}\ {\isasymrightarrow}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}.  This is
+  isomorphic to the encoding via tuples \isa{{\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymtimes}\ {\isasymdots}\ {\isasymtimes}\ {\isasymtau}\isactrlsub n\ {\isasymrightarrow}\ {\isasymtau}}, but
+  the curried version fits more smoothly into the basic
+  calculus.\footnote{The difference is even more significant in
+  higher-order logic, because additional the redundant tuple structure
+  needs to be accommodated by formal reasoning.}
+
+  Currying gives some flexiblity due to \emph{partial application}.  A
+  function \isa{f{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}\ {\isasymrightarrow}\ {\isasymtau}\isactrlbsub {\isadigit{2}}\isactrlesub \ {\isasymrightarrow}\ {\isasymtau}} can be applied to \isa{x{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{1}}}
+  and the remaining \isa{{\isacharparenleft}f\ x{\isacharparenright}{\isacharcolon}\ {\isasymtau}\isactrlsub {\isadigit{2}}\ {\isasymrightarrow}\ {\isasymtau}} passed to other functions
+  etc.  How well this works in practice depends on the order of
+  arguments.  In the worst case, arguments are arranged erratically,
+  and using a function in a certain situation always requires some
+  glue code.  Thus we would get exponentially many oppurtunities to
+  decorate the code with meaningless permutations of arguments.
+
+  This can be avoided by \emph{canonical argument order}, which
+  observes certain standard patterns of function definitions and
+  minimizes adhoc permutations in their application.  In Isabelle/ML,
+  large portions of non-trivial source code are written without ever
+  using the infamous function \isa{swap{\isacharcolon}\ {\isasymalpha}\ {\isasymtimes}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymtimes}\ {\isasymalpha}} or the
+  combinator \isa{C{\isacharcolon}\ {\isacharparenleft}{\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}\ {\isasymrightarrow}\ {\isacharparenleft}{\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymgamma}{\isacharparenright}}, which is not even
+  defined in our library.
+
+  \medskip The basic idea is that arguments that vary less are moved
+  further to the left than those that vary more.  Two particularly
+  important categories of functions are \emph{selectors} and
+  \emph{updates}.
+
+  The subsequent scheme is based on a hypothetical set-like container
+  of type \isa{{\isasymbeta}} that manages elements of type \isa{{\isasymalpha}}.  Both
+  the names and types of the associated operations are canonical for
+  Isabelle/ML.
+
+  \medskip
+  \begin{tabular}{ll}
+  kind & canonical name and type \\\hline
+  selector & \isa{member{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymalpha}\ {\isasymrightarrow}\ bool} \\
+  update & \isa{insert{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} \\
+  \end{tabular}
+  \medskip
+
+  Given a container \isa{B{\isacharcolon}\ {\isasymbeta}}, the partially applied \isa{member\ B} is a predicate over elements \isa{{\isasymalpha}\ {\isasymrightarrow}\ bool}, and
+  thus represents the intended denotation directly.  It is customary
+  to pass the abstract predicate to further operations, not the
+  concrete container.  The argument order makes it easy to use other
+  combinators: \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}\ list} will check a list of
+  elements for membership in \isa{B} etc. Often the explicit
+  \isa{list} is pointless and can be contracted in the application
+  \isa{forall\ {\isacharparenleft}member\ B{\isacharparenright}} to get directly a predicate again.
+
+  The update operation naturally ``varies'' the container, so it moves
+  to the right: \isa{insert\ a} is a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} to
+  insert a value \isa{a}.  These can be composed naturally as
+  follows: \isa{insert\ c\ {\isasymcirc}\ insert\ b\ {\isasymcirc}\ insert\ a}.  This works well,
+  apart from some awkwardness due to conventional mathematical
+  function composition, which can be easily amended as follows.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Forward application and composition%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Regular function application and infix notation works best for
+  relatively deeply structured expressions, e.g.\ \isa{h\ {\isacharparenleft}f\ x\ y\ {\isacharplus}\ g\ z{\isacharparenright}}.  The important special case if \emph{linear transformation}
+  applies a cascade of functions as follows: \isa{f\isactrlsub n\ {\isacharparenleft}{\isasymdots}\ {\isacharparenleft}f\isactrlsub {\isadigit{1}}\ x{\isacharparenright}{\isacharparenright}}.
+  This becomes hard to read and maintain if the functions are
+  themselves complex expressions.  The notation can be significantly
+  improved by introducing \emph{forward} versions of application and
+  composition as follows:
+
+  \medskip
+  \begin{tabular}{lll}
+  \isa{x\ {\isacharbar}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x} \\
+  \isa{f\ {\isacharhash}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isachargreater}\ g} \\
+  \end{tabular}
+  \medskip
+
+  This enables to write conveniently \isa{x\ {\isacharbar}{\isachargreater}\ f\isactrlsub {\isadigit{1}}\ {\isacharbar}{\isachargreater}\ {\isasymdots}\ {\isacharbar}{\isachargreater}\ f\isactrlsub n} or
+  \isa{f\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\isactrlsub n} for its functional abstraction over \isa{x}.
+
+  \medskip There is an additional set of combinators to accommodate
+  multiple results (via pairs) that are passed on as multiple
+  arguments (via currying).
+
+  \medskip
+  \begin{tabular}{lll}
+  \isa{{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharbar}{\isacharminus}{\isachargreater}\ f} & \isa{{\isasymequiv}} & \isa{f\ x\ y} \\
+  \isa{f\ {\isacharhash}{\isacharminus}{\isachargreater}\ g} & \isa{{\isasymequiv}} & \isa{x\ {\isacharbar}{\isachargreater}\ f\ {\isacharbar}{\isacharminus}{\isachargreater}\ g} \\
+  \end{tabular}
+  \medskip%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{$\mid$$>$}\verb|op |\verb,|,\verb|>  : 'a * ('a -> 'b) -> 'b| \\
+  \indexdef{}{ML}{$\mid$-$>$}\verb|op |\verb,|,\verb|->  : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
+  \indexdef{}{ML}{\#$>$}\verb|op #>  : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
+  \indexdef{}{ML}{\#-$>$}\verb|op #->  : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
+  \end{mldecls}
+
+  %FIXME description!?%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Canonical iteration%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As explained above, a function \isa{f{\isacharcolon}\ {\isasymalpha}\ {\isasymrightarrow}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} can be
+  understood as update on a configuration of type \isa{{\isasymbeta}} that is
+  parametrized by arguments of type \isa{{\isasymalpha}}.  Given \isa{a{\isacharcolon}\ {\isasymalpha}}
+  the partial application \isa{{\isacharparenleft}f\ a{\isacharparenright}{\isacharcolon}\ {\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}} operates
+  homogeneously on \isa{{\isasymbeta}}.  This can be iterated naturally over a
+  list of parameters \isa{{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isacharbrackright}} as \isa{f\ a\isactrlsub {\isadigit{1}}\ {\isacharhash}{\isachargreater}\ {\isasymdots}\ {\isacharhash}{\isachargreater}\ f\ a\isactrlbsub n\isactrlesub \isactrlbsub \isactrlesub }.  The latter expression is again a function \isa{{\isasymbeta}\ {\isasymrightarrow}\ {\isasymbeta}}.
+  It can be applied to an initial configuration \isa{b{\isacharcolon}\ {\isasymbeta}} to
+  start the iteration over the given list of arguments: each \isa{a} in \isa{a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n} is applied consecutively by updating a
+  cumulative configuration.
+
+  The \isa{fold} combinator in Isabelle/ML lifts a function \isa{f} as above to its iterated version over a list of arguments.
+  Lifting can be repeated, e.g.\ \isa{{\isacharparenleft}fold\ {\isasymcirc}\ fold{\isacharparenright}\ f} iterates
+  over a list of lists as expected.
+
+  The variant \isa{fold{\isacharunderscore}rev} works inside-out over the list of
+  arguments, such that \isa{fold{\isacharunderscore}rev\ f\ {\isasymequiv}\ fold\ f\ {\isasymcirc}\ rev} holds.
+
+  The \isa{fold{\isacharunderscore}map} combinator essentially performs \isa{fold} and \isa{map} simultaneously: each application of \isa{f} produces an updated configuration together with a side-result;
+  the iteration collects all such side-results as a separate list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
+  \indexdef{}{ML}{fold\_rev}\verb|fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
+  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|fold|~\isa{f} lifts the parametrized update function
+  \isa{f} to a list of parameters.
+
+  \item \verb|fold_rev|~\isa{f} is similar to \verb|fold|~\isa{f}, but works inside-out.
+
+  \item \verb|fold_map|~\isa{f} lifts the parametrized update
+  function \isa{f} (with side-result) to a list of parameters and
+  cumulative side-results.
+
+  \end{description}
+
+  \begin{warn}
+  The literature on functional programming provides a multitude of
+  combinators called \isa{foldl}, \isa{foldr} etc.  SML97
+  provides its own variations as \verb|List.foldl| and \verb|List.foldr|, while the classic Isabelle library still has the
+  slightly more convenient historic \verb|Library.foldl| and \verb|Library.foldr|.  To avoid further confusion, all of this should be
+  ignored, and \verb|fold| (or \verb|fold_rev|) used exclusively.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example shows how to fill a text buffer
+  incrementally by adding strings, either individually or from a given
+  list.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ s\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}add\ {\isachardoublequote}digits{\isacharcolon}\ {\isachardoublequote}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ fold\ {\isacharparenleft}Buffer{\isachardot}add\ o\ string{\isacharunderscore}of{\isacharunderscore}int{\isacharparenright}\ {\isacharparenleft}{\isadigit{0}}\ upto\ {\isadigit{9}}{\isacharparenright}\isanewline
+\ \ \ \ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}s\ {\isacharequal}\ {\isachardoublequote}digits{\isacharcolon}\ {\isadigit{0}}{\isadigit{1}}{\isadigit{2}}{\isadigit{3}}{\isadigit{4}}{\isadigit{5}}{\isadigit{6}}{\isadigit{7}}{\isadigit{8}}{\isadigit{9}}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Note how \verb|fold (Buffer.add o string_of_int)| above saves
+  an extra \verb|map| over the given list.  This kind of peephole
+  optimization reduces both the code size and the tree structures in
+  memory (``deforestation''), but requires some practice to read and
+  write it fluently.
+
+  \medskip The next example elaborates this idea and demonstrates fast
+  accumulation of tree content using a text buffer.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ datatype\ tree\ {\isacharequal}\ Text\ of\ string\ {\isacharbar}\ Elem\ of\ string\ {\isacharasterisk}\ tree\ list{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ slow{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ txt\isanewline
+\ \ \ \ {\isacharbar}\ slow{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ implode\ {\isacharparenleft}map\ slow{\isacharunderscore}content\ ts{\isacharparenright}\ {\isacharcircum}\isanewline
+\ \ \ \ \ \ \ \ {\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}\isanewline
+\isanewline
+\ \ fun\ add{\isacharunderscore}content\ {\isacharparenleft}Text\ txt{\isacharparenright}\ {\isacharequal}\ Buffer{\isachardot}add\ txt\isanewline
+\ \ \ \ {\isacharbar}\ add{\isacharunderscore}content\ {\isacharparenleft}Elem\ {\isacharparenleft}name{\isacharcomma}\ ts{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ fold\ add{\isacharunderscore}content\ ts\ {\isacharhash}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ Buffer{\isachardot}add\ {\isacharparenleft}{\isachardoublequote}{\isacharless}{\isacharslash}{\isachardoublequote}\ {\isacharcircum}\ name\ {\isacharcircum}\ {\isachardoublequote}{\isachargreater}{\isachardoublequote}{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ fun\ fast{\isacharunderscore}content\ tree\ {\isacharequal}\isanewline
+\ \ \ \ Buffer{\isachardot}empty\ {\isacharbar}{\isachargreater}\ add{\isacharunderscore}content\ tree\ {\isacharbar}{\isachargreater}\ Buffer{\isachardot}content{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The slow part of \verb|slow_content| is the \verb|implode| of
+  the recursive results, because it copies previously produced strings
+  afresh.
+
+  The incremental \verb|add_content| avoids this by operating on a
+  buffer that is passed-through in a linear fashion.  Using \verb|#>| and contraction over the actual \verb|Buffer.T| argument
+  saves some additional boiler-plate, but requires again some
+  practice.  Of course, the two \verb|Buffer.add| invocations with
+  concatenated strings could have been split into smaller parts, but
+  this would have obfuscated the source without making a big
+  difference in allocations.  Here we have done some
+  peephole-optimization for the sake of readability.
+
+  Another benefit of \verb|add_content| is its ``open'' form as a
+  function on \verb|Buffer.T| that can be continued in further
+  linear transformations, folding etc.  Thus it is more compositional
+  than the naive \verb|slow_content|.  As a realistic example, compare
+  the slightly old-style \verb|Term.maxidx_of_term: term -> int| with
+  the newer \verb|Term.maxidx_term: term -> int -> int| in
+  Isabelle/Pure.
+
+  Note that \verb|fast_content| above is only defined for completeness
+  of the example.  In many practical situations, it is customary to
+  defined the incremental \verb|add_content| only and leave the
+  initialization and termination to the concrete application by the
+  user.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Message output channels \label{sec:message-channels}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle provides output channels for different kinds of
+  messages: regular output, high-volume tracing information, warnings,
+  and errors.
+
+  Depending on the user interface involved, these messages may appear
+  in different text styles or colours.  The standard output for
+  terminal sessions prefixes each line of warnings by \verb|###| and errors by \verb|***|, but leaves anything else
+  unchanged.
+
+  Messages are associated with the transaction context of the running
+  Isar command.  This enables the front-end to manage commands and
+  resulting messages together.  For example, after deleting a command
+  from a given theory document version, the corresponding message
+  output can be retracted from the display.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{writeln}\verb|writeln: string -> unit| \\
+  \indexdef{}{ML}{tracing}\verb|tracing: string -> unit| \\
+  \indexdef{}{ML}{warning}\verb|warning: string -> unit| \\
+  \indexdef{}{ML}{error}\verb|error: string -> 'a| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|writeln|~\isa{text} outputs \isa{text} as regular
+  message.  This is the primary message output operation of Isabelle
+  and should be used by default.
+
+  \item \verb|tracing|~\isa{text} outputs \isa{text} as special
+  tracing message, indicating potential high-volume output to the
+  front-end (hundreds or thousands of messages issued by a single
+  command).  The idea is to allow the user-interface to downgrade the
+  quality of message display to achieve higher throughput.
+
+  Note that the user might have to take special actions to see tracing
+  output, e.g.\ switch to a different output window.  So this channel
+  should not be used for regular output.
+
+  \item \verb|warning|~\isa{text} outputs \isa{text} as
+  warning, which typically means some extra emphasis on the front-end
+  side (color highlighting, icon).
+
+  \item \verb|error|~\isa{text} raises exception \verb|ERROR|~\isa{text} and thus lets the Isar toplevel print \isa{text} on the
+  error channel, which typically means some extra emphasis on the
+  front-end side (color highlighting, icon).
+
+  This assumes that the exception is not handled before the command
+  terminates.  Handling exception \verb|ERROR|~\isa{text} is a
+  perfectly legal alternative: it means that the error is absorbed
+  without any message output.
+
+  \begin{warn}
+  The actual error channel is accessed via \verb|Output.error_msg|, but
+  the interaction protocol of Proof~General \emph{crashes} if that
+  function is used in regular ML code: error output and toplevel
+  command failure always need to coincide here.
+  \end{warn}
+
+  \end{description}
+
+  \begin{warn}
+  Regular Isabelle/ML code should output messages exclusively by the
+  official channels.  Using raw I/O on \emph{stdout} or \emph{stderr}
+  instead (e.g.\ via \verb|TextIO.output|) is apt to cause problems in
+  the presence of parallel and asynchronous processing of Isabelle
+  theories.  Such raw output might be displayed by the front-end in
+  some system console log, with a low chance that the user will ever
+  see it.  Moreover, as a genuine side-effect on global process
+  channels, there is no proper way to retract output when Isar command
+  transactions are reset.
+  \end{warn}
+
+  \begin{warn}
+  The message channels should be used in a message-oriented manner.
+  This means that multi-line output that logically belongs together
+  needs to be issued by a \emph{single} invocation of \verb|writeln|
+  etc.  with the functional concatenation of all message constituents.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example demonstrates a multi-line
+  warning.  Note that in some situations the user sees only the first
+  line, so the most important point should be made first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML{\isacharunderscore}command}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ warning\ {\isacharparenleft}cat{\isacharunderscore}lines\isanewline
+\ \ \ {\isacharbrackleft}{\isachardoublequote}Beware\ the\ Jabberwock{\isacharcomma}\ my\ son{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ jaws\ that\ bite{\isacharcomma}\ the\ claws\ that\ catch{\isacharbang}{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}Beware\ the\ Jubjub\ Bird{\isacharcomma}\ and\ shun{\isachardoublequote}{\isacharcomma}\isanewline
+\ \ \ \ {\isachardoublequote}The\ frumious\ Bandersnatch{\isacharbang}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsection{Exceptions \label{sec:exceptions}%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Recent versions of Poly/ML (5.2.1 or later) support robust
-  multithreaded execution, based on native operating system threads of
-  the underlying platform.  Thus threads will actually be executed in
-  parallel on multi-core systems.  A speedup-factor of approximately
-  1.5--3 can be expected on a regular 4-core machine.\footnote{There
-  is some inherent limitation of the speedup factor due to garbage
-  collection, which is still sequential.  It helps to provide initial
-  heap space generously, using the \texttt{-H} option of Poly/ML.}
-  Threads also help to organize advanced operations of the system,
-  with explicit communication between sub-components, real-time
-  conditions, time-outs etc.
+The Standard ML semantics of strict functional evaluation
+  together with exceptions is rather well defined, but some delicate
+  points need to be observed to avoid that ML programs go wrong
+  despite static type-checking.  Exceptions in Isabelle/ML are
+  subsequently categorized as follows.
+
+  \paragraph{Regular user errors.}  These are meant to provide
+  informative feedback about malformed input etc.
+
+  The \emph{error} function raises the corresponding \emph{ERROR}
+  exception, with a plain text message as argument.  \emph{ERROR}
+  exceptions can be handled internally, in order to be ignored, turned
+  into other exceptions, or cascaded by appending messages.  If the
+  corresponding Isabelle/Isar command terminates with an \emph{ERROR}
+  exception state, the toplevel will print the result on the error
+  channel (see \secref{sec:message-channels}).
+
+  It is considered bad style to refer to internal function names or
+  values in ML source notation in user error messages.
+
+  Grammatical correctness of error messages can be improved by
+  \emph{omitting} final punctuation: messages are often concatenated
+  or put into a larger context (e.g.\ augmented with source position).
+  By not insisting in the final word at the origin of the error, the
+  system can perform its administrative tasks more easily and
+  robustly.
+
+  \paragraph{Program failures.}  There is a handful of standard
+  exceptions that indicate general failure situations, or failures of
+  core operations on logical entities (types, terms, theorems,
+  theories, see \chref{ch:logic}).
+
+  These exceptions indicate a genuine breakdown of the program, so the
+  main purpose is to determine quickly what has happened where.
+  Traditionally, the (short) exception message would include the name
+  of an ML function, although this no longer necessary, because the ML
+  runtime system prints a detailed source position of the
+  corresponding \verb|raise| keyword.
+
+  \medskip User modules can always introduce their own custom
+  exceptions locally, e.g.\ to organize internal failures robustly
+  without overlapping with existing exceptions.  Exceptions that are
+  exposed in module signatures require extra care, though, and should
+  \emph{not} be introduced by default.  Surprise by end-users or ML
+  users of a module can be often minimized by using plain user errors.
+
+  \paragraph{Interrupts.}  These indicate arbitrary system events:
+  both the ML runtime system and the Isabelle/ML infrastructure signal
+  various exceptional situations by raising the special
+  \emph{Interrupt} exception in user code.
+
+  This is the one and only way that physical events can intrude an
+  Isabelle/ML program.  Such an interrupt can mean out-of-memory,
+  stack overflow, timeout, internal signaling of threads, or the user
+  producing a console interrupt manually etc.  An Isabelle/ML program
+  that intercepts interrupts becomes dependent on physical effects of
+  the environment.  Even worse, exception handling patterns that are
+  too general by accident, e.g.\ by mispelled exception constructors,
+  will cover interrupts unintentionally, and thus render the program
+  semantics ill-defined.
+
+  Note that the Interrupt exception dates back to the original SML90
+  language definition.  It was excluded from the SML97 version to
+  avoid its malign impact on ML program semantics, but without
+  providing a viable alternative.  Isabelle/ML recovers physical
+  interruptibility (which an indispensable tool to implement managed
+  evaluation of Isar command transactions), but requires user code to
+  be strictly transparent wrt.\ interrupts.
+
+  \begin{warn}
+  Isabelle/ML user code needs to terminate promptly on interruption,
+  without guessing at its meaning to the system infrastructure.
+  Temporary handling of interrupts for cleanup of global resources
+  etc.\ needs to be followed immediately by re-raising of the original
+  exception.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
+  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
+  \indexdef{}{ML}{ERROR}\verb|ERROR: string -> exn| \\
+  \indexdef{}{ML}{Fail}\verb|Fail: string -> exn| \\
+  \indexdef{}{ML}{Exn.is\_interrupt}\verb|Exn.is_interrupt: exn -> bool| \\
+  \indexdef{}{ML}{reraise}\verb|reraise: exn -> 'a| \\
+  \indexdef{}{ML}{exception\_trace}\verb|exception_trace: (unit -> 'a) -> 'a| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|try|~\isa{f\ x} makes the partiality of evaluating
+  \isa{f\ x} explicit via the option datatype.  Interrupts are
+  \emph{not} handled here, i.e.\ this form serves as safe replacement
+  for the \emph{unsafe} version \verb|(SOME|~\isa{f\ x}~\verb|handle _ => NONE)| that is occasionally seen in
+  books about SML.
+
+  \item \verb|can| is similar to \verb|try| with more abstract result.
+
+  \item \verb|ERROR|~\isa{msg} represents user errors; this
+  exception is always raised via the \verb|error| function (see
+  \secref{sec:message-channels}).
+
+  \item \verb|Fail|~\isa{msg} represents general program failures.
+
+  \item \verb|Exn.is_interrupt| identifies interrupts robustly, without
+  mentioning concrete exception constructors in user code.  Handled
+  interrupts need to be re-raised promptly!
+
+  \item \verb|reraise|~\isa{exn} raises exception \isa{exn}
+  while preserving its implicit position information (if possible,
+  depending on the ML platform).
+
+  \item \verb|exception_trace|~\verb|(fn _ =>|~\isa{e}\verb|)| evaluates expression \isa{e} while printing
+  a full trace of its stack of nested exceptions (if possible,
+  depending on the ML platform).\footnote{In various versions of
+  Poly/ML the trace will appear on raw stdout of the Isabelle
+  process.}
+
+  Inserting \verb|exception_trace| into ML code temporarily is useful
+  for debugging, but not suitable for production code.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isatagmlantiq
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+  \indexdef{}{ML antiquotation}{assert}\hypertarget{ML antiquotation.assert}{\hyperlink{ML antiquotation.assert}{\mbox{\isa{assert}}}} & : & \isa{ML{\isacharunderscore}antiquotation} \\
+  \end{matharray}
+
+  \begin{description}
+
+  \item \isa{{\isacharat}{\isacharbraceleft}assert{\isacharbraceright}} inlines a function \isa{bool\ {\isasymRightarrow}\ unit}
+  that raises \verb|Fail| if the argument is \verb|false|.  Due to
+  inlining the source position of failed assertions is included in the
+  error output.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlantiq
+{\isafoldmlantiq}%
+%
+\isadelimmlantiq
+%
+\endisadelimmlantiq
+%
+\isamarkupsection{Basic data types%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The basis library proposal of SML97 need to be treated with
+  caution.  Many of its operations simply do not fit with important
+  Isabelle/ML conventions (like ``canonical argument order'', see
+  \secref{sec:canonical-argument-order}), others can cause serious
+  problems with the parallel evaluation model of Isabelle/ML (such as
+  \verb|TextIO.print| or \verb|OS.Process.system|).
+
+  Subsequently we give a brief overview of important operations on
+  basic ML data types.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Characters%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{char}\verb|type char| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type \verb|char| is \emph{not} used.  The smallest textual
+  unit in Isabelle is represented a ``symbol'' (see
+  \secref{sec:symbols}).
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Integers%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{int}\verb|type int| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item Type \verb|int| represents regular mathematical integers,
+  which are \emph{unbounded}.  Overflow never happens in
+  practice.\footnote{The size limit for integer bit patterns in memory
+  is 64\,MB for 32-bit Poly/ML, and much higher for 64-bit systems.}
+  This works uniformly for all supported ML platforms (Poly/ML and
+  SML/NJ).
+
+  Literal integers in ML text (e.g.\ \verb|123456789012345678901234567890|) are forced to be of this one true
+  integer type --- overloading of SML97 is disabled.
+
+  Structure \verb|IntInf| of SML97 is obsolete, always use
+  \verb|Int|.  Structure \verb|Integer| in \hyperlink{file.~~/src/Pure/General/integer.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}integer{\isachardot}ML}}}} provides some additional
+  operations.
 
-  Threads lack the memory protection of separate processes, and
-  operate concurrently on shared heap memory.  This has the advantage
-  that results of independent computations are immediately available
-  to other threads, without requiring untyped character streams,
-  awkward serialization etc.
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Options%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{Option.map}\verb|Option.map: ('a -> 'b) -> 'a option -> 'b option| \\
+  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
+  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
+  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
+  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
+  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
+  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+Apart from \verb|Option.map| most operations defined in
+  structure \verb|Option| are alien to Isabelle/ML.  The
+  operations shown above are defined in \hyperlink{file.~~/src/Pure/General/basics.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}basics{\isachardot}ML}}}}, among others.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Lists are ubiquitous in ML as simple and light-weight
+  ``collections'' for many everyday programming tasks.  Isabelle/ML
+  provides important additions and improvements over operations that
+  are predefined in the SML97 library.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{cons}\verb|cons: 'a -> 'a list -> 'a list| \\
+  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
+  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
+  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
+  \indexdef{}{ML}{update}\verb|update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|cons|~\isa{x\ xs} evaluates to \isa{x\ {\isacharcolon}{\isacharcolon}\ xs}.
+
+  Tupled infix operators are a historical accident in Standard ML.
+  The curried \verb|cons| amends this, but it should be only used when
+  partial application is required.
+
+  \item \verb|member|, \verb|insert|, \verb|remove|, \verb|update| treat
+  lists as a set-like container that maintains the order of elements.
+  See \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\isachardot}ML}}}} for the full specifications
+  (written in ML).  There are some further derived operations like
+  \verb|union| or \verb|inter|.
+
+  Note that \verb|insert| is conservative about elements that are
+  already a \verb|member| of the list, while \verb|update| ensures that
+  the last entry is always put in front.  The latter discipline is
+  often more appropriate in declarations of context data
+  (\secref{sec:context-data}) that are issued by the user in Isar
+  source: more recent declarations normally take precedence over
+  earlier ones.
 
-  On the other hand, some programming guidelines need to be observed
-  in order to make unprotected parallelism work out smoothly.  While
-  the ML system implementation is responsible to maintain basic
-  integrity of the representation of ML values in memory, the
-  application programmer needs to ensure that multithreaded execution
-  does not break the intended semantics.
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+Using canonical \verb|fold| together with canonical \verb|cons|, or similar standard operations, alternates the orientation of
+  data.  The is quite natural and should not altered forcible by
+  inserting extra applications \verb|rev|.  The alternative \verb|fold_rev| can be used in the relatively few situations, where
+  alternation should be prevented.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ items\ {\isacharequal}\ {\isacharbrackleft}{\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharcomma}\ {\isadigit{3}}{\isacharcomma}\ {\isadigit{4}}{\isacharcomma}\ {\isadigit{5}}{\isacharcomma}\ {\isadigit{6}}{\isacharcomma}\ {\isadigit{7}}{\isacharcomma}\ {\isadigit{8}}{\isacharcomma}\ {\isadigit{9}}{\isacharcomma}\ {\isadigit{1}}{\isadigit{0}}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{1}}\ {\isacharequal}\ fold\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{1}}\ {\isacharequal}\ rev\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+\isanewline
+\ \ val\ list{\isadigit{2}}\ {\isacharequal}\ fold{\isacharunderscore}rev\ cons\ items\ {\isacharbrackleft}{\isacharbrackright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}list{\isadigit{2}}\ {\isacharequal}\ items{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+The subsequent example demonstrates how to \emph{merge} two
+  lists in a natural way.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ fun\ merge{\isacharunderscore}lists\ eq\ {\isacharparenleft}xs{\isacharcomma}\ ys{\isacharparenright}\ {\isacharequal}\ fold{\isacharunderscore}rev\ {\isacharparenleft}insert\ eq{\isacharparenright}\ ys\ xs{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\begin{isamarkuptext}%
+Here the first list is treated conservatively: only the new
+  elements from the second list are inserted.  The inside-out order of
+  insertion via \verb|fold_rev| attempts to preserve the order of
+  elements in the result.
+
+  This way of merging lists is typical for context data
+  (\secref{sec:context-data}).  See also \verb|merge| as defined in
+  \hyperlink{file.~~/src/Pure/library.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}library{\isachardot}ML}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Association lists%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The operations for association lists interpret a concrete list
+  of pairs as a finite function from keys to values.  Redundant
+  representations with multiple occurrences of the same key are
+  implicitly normalized: lookup and update only take the first
+  occurrence into account.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
+  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
+  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|AList.lookup|, \verb|AList.defined|, \verb|AList.update|
+  implement the main ``framework operations'' for mappings in
+  Isabelle/ML, with standard conventions for names and types.
+
+  Note that a function called \isa{lookup} is obliged to express its
+  partiality via an explicit option element.  There is no choice to
+  raise an exception, without changing the name to something like
+  \isa{the{\isacharunderscore}element} or \isa{get}.
+
+  The \isa{defined} operation is essentially a contraction of \verb|is_some| and \isa{lookup}, but this is sufficiently frequent to
+  justify its independent existence.  This also gives the
+  implementation some opportunity for peep-hole optimization.
+
+  \end{description}
 
-  \medskip \paragraph{Critical shared resources.} Actually only those
-  parts outside the purely functional world of ML are critical.  In
-  particular, this covers
+  Association lists are adequate as simple and light-weight
+  implementation of finite mappings in many practical situations.  A
+  more heavy-duty table structure is defined in \hyperlink{file.~~/src/Pure/General/table.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}General{\isacharslash}table{\isachardot}ML}}}}; that version scales easily to
+  thousands or millions of elements.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Unsynchronized references%
+}
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML type}{Unsynchronized.ref}\verb|type 'a Unsynchronized.ref| \\
+  \indexdef{}{ML}{Unsynchronized.ref}\verb|Unsynchronized.ref: 'a -> 'a Unsynchronized.ref| \\
+  \indexdef{}{ML}{!}\verb|! : 'a Unsynchronized.ref -> 'a| \\
+  \indexdef{}{ML}{:=}\verb|op := : 'a Unsynchronized.ref * 'a -> unit| \\
+  \end{mldecls}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\begin{isamarkuptext}%
+Due to ubiquitous parallelism in Isabelle/ML (see also
+  \secref{sec:multi-threading}), the mutable reference cells of
+  Standard ML are notorious for causing problems.  In a highly
+  parallel system, both correctness \emph{and} performance are easily
+  degraded when using mutable data.
+
+  The unwieldy name of \verb|Unsynchronized.ref| for the constructor
+  for references in Isabelle/ML emphasizes the inconveniences caused by
+  mutability.  Existing operations \verb|!|  and \verb|op :=| are
+  unchanged, but should be used with special precautions, say in a
+  strictly local situation that is guaranteed to be restricted to
+  sequential evaluation --- now and in the future.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Thread-safe programming \label{sec:multi-threading}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Multi-threaded execution has become an everyday reality in
+  Isabelle since Poly/ML 5.2.1 and Isabelle2008.  Isabelle/ML provides
+  implicit and explicit parallelism by default, and there is no way
+  for user-space tools to ``opt out''.  ML programs that are purely
+  functional, output messages only via the official channels
+  (\secref{sec:message-channels}), and do not intercept interrupts
+  (\secref{sec:exceptions}) can participate in the multi-threaded
+  environment immediately without further ado.
+
+  More ambitious tools with more fine-grained interaction with the
+  environment need to observe the principles explained below.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Multi-threading with shared memory%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Multiple threads help to organize advanced operations of the
+  system, such as real-time conditions on command transactions,
+  sub-components with explicit communication, general asynchronous
+  interaction etc.  Moreover, parallel evaluation is a prerequisite to
+  make adequate use of the CPU resources that are available on
+  multi-core systems.\footnote{Multi-core computing does not mean that
+  there are ``spare cycles'' to be wasted.  It means that the
+  continued exponential speedup of CPU performance due to ``Moore's
+  Law'' follows different rules: clock frequency has reached its peak
+  around 2005, and applications need to be parallelized in order to
+  avoid a perceived loss of performance.  See also
+  \cite{Sutter:2005}.}
+
+  Isabelle/Isar exploits the inherent structure of theories and proofs
+  to support \emph{implicit parallelism} to a large extent.  LCF-style
+  theorem provides almost ideal conditions for that; see also
+  \cite{Wenzel:2009}.  This means, significant parts of theory and
+  proof checking is parallelized by default.  A maximum speedup-factor
+  of 3.0 on 4 cores and 5.0 on 8 cores can be
+  expected.\footnote{Further scalability is limited due to garbage
+  collection, which is still sequential in Poly/ML 5.2/5.3/5.4.  It
+  helps to provide initial heap space generously, using the
+  \texttt{-H} option.  Initial heap size needs to be scaled-up
+  together with the number of CPU cores: approximately 1--2\,GB per
+  core..}
+
+  \medskip ML threads lack the memory protection of separate
+  processes, and operate concurrently on shared heap memory.  This has
+  the advantage that results of independent computations are
+  immediately available to other threads: abstract values can be
+  passed between threads without copying or awkward serialization that
+  is typically required for explicit message passing between separate
+  processes.
+
+  To make shared-memory multi-threading work robustly and efficiently,
+  some programming guidelines need to be observed.  While the ML
+  system is responsible to maintain basic integrity of the
+  representation of ML values in memory, the application programmer
+  needs to ensure that multi-threaded execution does not break the
+  intended semantics.
+
+  \begin{warn}
+  To participate in implicit parallelism, tools need to be
+  thread-safe.  A single ill-behaved tool can affect the stability and
+  performance of the whole system.
+  \end{warn}
+
+  Apart from observing the principles of thread-safeness passively,
+  advanced tools may also exploit parallelism actively, e.g.\ by using
+  ``future values'' (\secref{sec:futures}) or the more basic library
+  functions for parallel list operations (\secref{sec:parlist}).
+
+  \begin{warn}
+  Parallel computing resources are managed centrally by the
+  Isabelle/ML infrastructure.  User programs must not fork their own
+  ML threads to perform computations.
+  \end{warn}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Critical shared resources%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Thread-safeness is mainly concerned about concurrent
+  read/write access to shared resources, which are outside the purely
+  functional world of ML.  This covers the following in particular.
 
   \begin{itemize}
 
-  \item global references (or arrays), i.e.\ those that persist over
-  several invocations of associated operations,\footnote{This is
-  independent of the visibility of such mutable values in the toplevel
-  scope.}
+  \item Global references (or arrays), i.e.\ mutable memory cells that
+  persist over several invocations of associated
+  operations.\footnote{This is independent of the visibility of such
+  mutable values in the toplevel scope.}
 
-  \item direct I/O on shared channels, notably \isa{stdin}, \isa{stdout}, \isa{stderr}.
+  \item Global state of the running Isabelle/ML process, i.e.\ raw I/O
+  channels, environment variables, current working directory.
+
+  \item Writable resources in the file-system that are shared among
+  different threads or other processes.
 
   \end{itemize}
 
-  The majority of tools implemented within the Isabelle/Isar framework
-  will not require any of these critical elements: nothing special
-  needs to be observed when staying in the purely functional fragment
-  of ML.  Note that output via the official Isabelle channels does not
-  count as direct I/O, so the operations \verb|writeln|, \verb|warning|, \verb|tracing| etc.\ are safe.
-
-  Moreover, ML bindings within the toplevel environment (\verb|type|, \verb|val|, \verb|structure| etc.) due to
-  run-time invocation of the compiler are also safe, because
-  Isabelle/Isar manages this as part of the theory or proof context.
-
-  \paragraph{Multithreading in Isabelle/Isar.}  The theory loader
-  automatically exploits the overall parallelism of independent nodes
-  in the development graph, as well as the inherent irrelevance of
-  proofs for goals being fully specified in advance.  This means,
-  checking of individual Isar proofs is parallelized by default.
-  Beyond that, very sophisticated proof tools may use local
-  parallelism internally, via the general programming model of
-  ``future values'' (see also \hyperlink{file.~~/src/Pure/Concurrent/future.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}future{\isachardot}ML}}}}).
-
-  Any ML code that works relatively to the present background theory
-  is already safe.  Contextual data may be easily stored within the
-  theory or proof context, thanks to the generic data concept of
-  Isabelle/Isar (see \secref{sec:context-data}).  This greatly
-  diminishes the demand for global state information in the first
-  place.
-
-  \medskip In rare situations where actual mutable content needs to be
-  manipulated, Isabelle provides a single \emph{critical section} that
-  may be entered while preventing any other thread from doing the
-  same.  Entering the critical section without contention is very
-  fast, and several basic system operations do so frequently.  This
-  also means that each thread should leave the critical section
-  quickly, otherwise parallel execution performance may degrade
-  significantly.
-
-  Despite this potential bottle-neck, centralized locking is
-  convenient, because it prevents deadlocks without demanding special
-  precautions.  Explicit communication demands other means, though.
-  The high-level abstraction of synchronized variables \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} enables parallel
-  components to communicate via shared state; see also \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} as canonical example.
-
-  \paragraph{Good conduct of impure programs.} The following
-  guidelines enable non-functional programs to participate in
-  multithreading.
+  Isabelle/ML provides various mechanisms to avoid critical shared
+  resources in most practical situations.  As last resort there are
+  some mechanisms for explicit synchronization.  The following
+  guidelines help to make Isabelle/ML programs work smoothly in a
+  concurrent environment.
 
   \begin{itemize}
 
-  \item Minimize global state information.  Using proper theory and
-  proof context data will actually return to functional update of
-  values, without any special precautions for multithreading.  Apart
-  from the fully general functors for theory and proof data (see
-  \secref{sec:context-data}) there are drop-in replacements that
-  emulate primitive references for common cases of \emph{configuration
-  options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
-  \verb|Named_Thms|).
+  \item Avoid global references altogether.  Isabelle/Isar maintains a
+  uniform context that incorporates arbitrary data declared by user
+  programs (\secref{sec:context-data}).  This context is passed as
+  plain value and user tools can get/map their own data in a purely
+  functional manner.  Configuration options within the context
+  (\secref{sec:config-options}) provide simple drop-in replacements
+  for formerly writable flags.
+
+  \item Keep components with local state information re-entrant.
+  Instead of poking initial values into (private) global references, a
+  new state record can be created on each invocation, and passed
+  through any auxiliary functions of the component.  The state record
+  may well contain mutable references, without requiring any special
+  synchronizations, as long as each invocation gets its own copy.
+
+  \item Avoid raw output on \isa{stdout} or \isa{stderr}.  The
+  Poly/ML library is thread-safe for each individual output operation,
+  but the ordering of parallel invocations is arbitrary.  This means
+  raw output will appear on some system console with unpredictable
+  interleaving of atomic chunks.
+
+  Note that this does not affect regular message output channels
+  (\secref{sec:message-channels}).  An official message is associated
+  with the command transaction from where it originates, independently
+  of other transactions.  This means each running Isar command has
+  effectively its own set of message channels, and interleaving can
+  only happen when commands use parallelism internally (and only at
+  message boundaries).
+
+  \item Treat environment variables and the current working directory
+  of the running process as strictly read-only.
 
-  \item Keep components with local state information
-  \emph{re-entrant}.  Instead of poking initial values into (private)
-  global references, create a new state record on each invocation, and
-  pass that through any auxiliary functions of the component.  The
-  state record may well contain mutable references, without requiring
-  any special synchronizations, as long as each invocation sees its
-  own copy.  Occasionally, one might even return to plain functional
-  updates on non-mutable record values here.
+  \item Restrict writing to the file-system to unique temporary files.
+  Isabelle already provides a temporary directory that is unique for
+  the running process, and there is a centralized source of unique
+  serial numbers in Isabelle/ML.  Thus temporary files that are passed
+  to to some external process will be always disjoint, and thus
+  thread-safe.
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexdef{}{ML}{File.tmp\_path}\verb|File.tmp_path: Path.T -> Path.T| \\
+  \indexdef{}{ML}{serial\_string}\verb|serial_string: unit -> string| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|File.tmp_path|~\isa{path} relocates the base
+  component of \isa{path} into the unique temporary directory of
+  the running Isabelle/ML process.
+
+  \item \verb|serial_string|~\isa{{\isacharparenleft}{\isacharparenright}} creates a new serial number
+  that is unique over the runtime of the Isabelle/ML process.
 
-  \item Isolate process configuration flags.  The main legitimate
-  application of global references is to configure the whole process
-  in a certain way, essentially affecting all threads.  A typical
-  example is the \verb|show_types| flag, which tells the pretty printer
-  to output explicit type information for terms.  Such flags usually
-  do not affect the functionality of the core system, but only the
-  view being presented to the user.
-
-  Occasionally, such global process flags are treated like implicit
-  arguments to certain operations, by using the \verb|setmp_CRITICAL| combinator
-  for safe temporary assignment.  Its traditional purpose was to
-  ensure proper recovery of the original value when exceptions are
-  raised in the body, now the functionality is extended to enter the
-  \emph{critical section} (with its usual potential of degrading
-  parallelism).
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isatagmlex
+%
+\begin{isamarkuptext}%
+The following example shows how to create unique
+  temporary file names.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlex
+{\isafoldmlex}%
+%
+\isadelimmlex
+%
+\endisadelimmlex
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ tmp{\isadigit{1}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ tmp{\isadigit{2}}\ {\isacharequal}\ File{\isachardot}tmp{\isacharunderscore}path\ {\isacharparenleft}Path{\isachardot}basic\ {\isacharparenleft}{\isachardoublequote}foo{\isachardoublequote}\ {\isacharcircum}\ serial{\isacharunderscore}string\ {\isacharparenleft}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}tmp{\isadigit{1}}\ {\isacharless}{\isachargreater}\ tmp{\isadigit{2}}{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
+%
+\isadelimML
+%
+\endisadelimML
+%
+\isamarkupsubsection{Explicit synchronization%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/ML also provides some explicit synchronization
+  mechanisms, for the rare situations where mutable shared resources
+  are really required.  These are based on the synchronizations
+  primitives of Poly/ML, which have been adapted to the specific
+  assumptions of the concurrent Isabelle/ML environment.  User code
+  must not use the Poly/ML primitives directly!
 
-  Note that recovery of plain value passing semantics via \verb|setmp_CRITICAL|~\isa{ref\ value} assumes that this \isa{ref} is
-  exclusively manipulated within the critical section.  In particular,
-  any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to
-  be marked critical as well, to prevent intruding another threads
-  local view, and a lost-update in the global scope, too.
+  \medskip The most basic synchronization concept is a single
+  \emph{critical section} (also called ``monitor'' in the literature).
+  A thread that enters the critical section prevents all other threads
+  from doing the same.  A thread that is already within the critical
+  section may re-enter it in an idempotent manner.
 
-  \end{itemize}
+  Such centralized locking is convenient, because it prevents
+  deadlocks by construction.
 
-  Recall that in an open ``LCF-style'' system like Isabelle/Isar, the
-  user participates in constructing the overall environment.  This
-  means that state-based facilities offered by one component will
-  require special caution later on.  So minimizing critical elements,
-  by staying within the plain value-oriented view relative to theory
-  or proof contexts most of the time, will also reduce the chance of
-  mishaps occurring to end-users.%
+  \medskip More fine-grained locking works via \emph{synchronized
+  variables}.  An explicit state component is associated with
+  mechanisms for locking and signaling.  There are operations to
+  await a condition, change the state, and signal the change to all
+  other waiting threads.
+
+  Here the synchronized access to the state variable is \emph{not}
+  re-entrant: direct or indirect nesting within the same thread will
+  cause a deadlock!%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -277,215 +2190,49 @@
 \begin{mldecls}
   \indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
   \indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
-  \indexdef{}{ML}{setmp\_CRITICAL}\verb|setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+  \end{mldecls}
+  \begin{mldecls}
+  \indexdef{}{ML type}{Synchronized.var}\verb|type 'a Synchronized.var| \\
+  \indexdef{}{ML}{Synchronized.var}\verb|Synchronized.var: string -> 'a -> 'a Synchronized.var| \\
+  \indexdef{}{ML}{Synchronized.guarded\_access}\verb|Synchronized.guarded_access: 'a Synchronized.var ->|\isasep\isanewline%
+\verb|  ('a -> ('b * 'a) option) -> 'b| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|NAMED_CRITICAL|~\isa{name\ f} evaluates \isa{f\ {\isacharparenleft}{\isacharparenright}}
-  while staying within the critical section of Isabelle/Isar.  No
-  other thread may do so at the same time, but non-critical parallel
-  execution will continue.  The \isa{name} argument serves for
-  diagnostic purposes and might help to spot sources of congestion.
+  \item \verb|NAMED_CRITICAL|~\isa{name\ e} evaluates \isa{e\ {\isacharparenleft}{\isacharparenright}}
+  within the central critical section of Isabelle/ML.  No other thread
+  may do so at the same time, but non-critical parallel execution will
+  continue.  The \isa{name} argument is used for tracing and might
+  help to spot sources of congestion.
+
+  Entering the critical section without contention is very fast, and
+  several basic system operations do so frequently.  Each thread
+  should leave the critical section quickly, otherwise parallel
+  performance may degrade.
 
   \item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
   name argument.
 
-  \item \verb|setmp_CRITICAL|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
-  while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily.  This recovers a value-passing
-  semantics involving global references, regardless of exceptions or
-  concurrency.
+  \item Type \verb|'a Synchronized.var| represents synchronized
+  variables with state of type \verb|'a|.
 
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupchapter{Basic library functions%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Beyond the proposal of the SML/NJ basis library, Isabelle comes
-  with its own library, from which selected parts are given here.
-  These should encourage a study of the Isabelle sources,
-  in particular files \emph{Pure/library.ML} and \emph{Pure/General/*.ML}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Linear transformations \label{sec:ML-linear-trans}%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{op $\mid$$>$ }\verb|op |\verb,|,\verb|> : 'a * ('a -> 'b) -> 'b| \\
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
-\begin{isamarkuptext}%
-\noindent Many problems in functional programming can be thought of
-  as linear transformations, i.e.~a caluclation starts with a
-  particular value \verb|x : foo| which is then transformed
-  by application of a function \verb|f : foo -> foo|,
-  continued by an application of a function \verb|g : foo -> bar|,
-  and so on.  As a canoncial example, take functions enriching
-  a theory by constant declararion and primitive definitions:
-
-  \smallskip\begin{mldecls}
-  \verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
-\verb|  -> theory -> term * theory| \\
-  \verb|Thm.add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory|
-  \end{mldecls}
-
-  \noindent Written with naive application, an addition of constant
-  \isa{bar} with type \isa{foo\ {\isasymRightarrow}\ foo} and
-  a corresponding definition \isa{bar\ {\isasymequiv}\ {\isasymlambda}x{\isachardot}\ x} would look like:
-
-  \smallskip\begin{mldecls}
-  \verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
-\verb|  (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
-\verb|    (Sign.declare_const|\isasep\isanewline%
-\verb|      ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
-  \end{mldecls}
+  \item \verb|Synchronized.var|~\isa{name\ x} creates a synchronized
+  variable that is initialized with value \isa{x}.  The \isa{name} is used for tracing.
 
-  \noindent With increasing numbers of applications, this code gets quite
-  unreadable.  Further, it is unintuitive that things are
-  written down in the opposite order as they actually ``happen''.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\noindent At this stage, Isabelle offers some combinators which allow
-  for more convenient notation, most notably reverse application:
-
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
-\verb|     (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{op $\mid$-$>$ }\verb|op |\verb,|,\verb|-> : ('c * 'a) * ('c -> 'a -> 'b) -> 'b| \\
-  \indexdef{}{ML}{op $\mid$$>$$>$ }\verb|op |\verb,|,\verb|>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c| \\
-  \indexdef{}{ML}{op $\mid$$\mid$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|> : ('c * 'a) * ('a -> 'b) -> 'c * 'b| \\
-  \indexdef{}{ML}{op $\mid$$\mid$$>$$>$ }\verb|op |\verb,|,\verb||\verb,|,\verb|>> : ('c * 'a) * ('a -> 'd * 'b) -> ('c * 'd) * 'b| \\
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent Usually, functions involving theory updates also return
-  side results; to use these conveniently, yet another
-  set of combinators is at hand, most notably \verb|op |\verb,|,\verb|->|
-  which allows curried access to side results:
+  \item \verb|Synchronized.guarded_access|~\isa{var\ f} lets the
+  function \isa{f} operate within a critical section on the state
+  \isa{x} as follows: if \isa{f\ x} produces \verb|NONE|, we
+  continue to wait on the internal condition variable, expecting that
+  some other thread will eventually change the content in a suitable
+  manner; if \isa{f\ x} produces \verb|SOME|~\isa{{\isacharparenleft}y{\isacharcomma}\ x{\isacharprime}{\isacharparenright}} we
+  are satisfied and assign the new state value \isa{x{\isacharprime}}, broadcast
+  a signal to all waiting threads on the associated condition
+  variable, and return the result \isa{y}.
 
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-
-  \end{mldecls}
-
-  \noindent \verb|op |\verb,|,\verb|>>| allows for processing side results on their own:
-
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
-
-  \end{mldecls}
-
-  \noindent Orthogonally, \verb|op |\verb,|,\verb||\verb,|,\verb|>| applies a transformation
-  in the presence of side results which are left unchanged:
+  \end{description}
 
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
-\verb|      (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|> Sign.restore_naming thy|\isasep\isanewline%
-
-  \end{mldecls}
-
-  \noindent \verb|op |\verb,|,\verb||\verb,|,\verb|>>| accumulates side results:
-
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
-\verb|      (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
-
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{fold}\verb|fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b| \\
-  \indexdef{}{ML}{fold\_map}\verb|fold_map: ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b| \\
-  \end{mldecls}%
+  There are some further variants of the general \verb|Synchronized.guarded_access| combinator, see \hyperlink{file.~~/src/Pure/Concurrent/synchronized.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}synchronized{\isachardot}ML}}}} for details.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
@@ -496,283 +2243,68 @@
 %
 \endisadelimmlref
 %
-\begin{isamarkuptext}%
-\noindent This principles naturally lift to \emph{lists} using
-  the \verb|fold| and \verb|fold_map| combinators.
-  The first lifts a single function
-  \begin{quote}\footnotesize
-    \verb|f : 'a -> 'b -> 'b| to \verb|'a list -> 'b -> 'b|
-  \end{quote}
-  such that
-  \begin{quote}\footnotesize
-    \verb|y |\verb,|,\verb|> fold f [x1, x2, ..., x_n]| \\
-    \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb|> f x2 |\verb,|,\verb|> ... |\verb,|,\verb|> f x_n|
-  \end{quote}
-  \noindent The second accumulates side results in a list by lifting
-  a single function
-  \begin{quote}\footnotesize
-    \verb|f : 'a -> 'b -> 'c * 'b| to \verb|'a list -> 'b -> 'c list * 'b|
-  \end{quote}
-  such that
-  \begin{quote}\footnotesize
-    \verb|y |\verb,|,\verb|> fold_map f [x1, x2, ..., x_n]| \\
-    \hspace*{2ex}\isa{{\isasymleadsto}} \verb|y |\verb,|,\verb|> f x1 |\verb,|,\verb||\verb,|,\verb|>> f x2 |\verb,|,\verb||\verb,|,\verb|>> ... |\verb,|,\verb||\verb,|,\verb|>> f x_n| \\
-    \hspace*{6ex}\verb||\verb,|,\verb||\verb,|,\verb|> (fn ((z1, z2), ..., z_n) => [z1, z2, ..., z_n])|
-  \end{quote}
-  
-  \noindent Example:
-
-  \smallskip\begin{mldecls}
-\verb|let|\isasep\isanewline%
-\verb|  val consts = ["foo", "bar"];|\isasep\isanewline%
-\verb|in|\isasep\isanewline%
-\verb|  thy|\isasep\isanewline%
-\verb|  |\verb,|,\verb|> fold_map (fn const => Sign.declare_const|\isasep\isanewline%
-\verb|       ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
-\verb|  |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
-\verb|  |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
-\verb|       Thm.add_def false false (Binding.empty, def)) defs)|\isasep\isanewline%
-\verb|end|
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimmlex
 %
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
+\endisadelimmlex
 %
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{op \#$>$ }\verb|op #> : ('a -> 'b) * ('b -> 'c) -> 'a -> 'c| \\
-  \indexdef{}{ML}{op \#-$>$ }\verb|op #-> : ('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd| \\
-  \indexdef{}{ML}{op \#$>$$>$ }\verb|op #>> : ('a -> 'c * 'b) * ('c -> 'd) -> 'a -> 'd * 'b| \\
-  \indexdef{}{ML}{op \#\#$>$ }\verb|op ##> : ('a -> 'c * 'b) * ('b -> 'd) -> 'a -> 'c * 'd| \\
-  \indexdef{}{ML}{op \#\#$>$$>$ }\verb|op ##>> : ('a -> 'c * 'b) * ('b -> 'e * 'd) -> 'a -> ('c * 'e) * 'd| \\
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\isatagmlex
 %
 \begin{isamarkuptext}%
-\noindent All those linear combinators also exist in higher-order
-  variants which do not expect a value on the left hand side
-  but a function.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{op ` }\verb|op ` : ('b -> 'a) -> 'b -> 'a * 'b| \\
-  \indexdef{}{ML}{tap}\verb|tap: ('b -> 'a) -> 'b -> 'b| \\
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\begin{isamarkuptext}%
-\noindent These operators allow to ``query'' a context
-  in a series of context transformations:
+See \hyperlink{file.~~/src/Pure/Concurrent/mailbox.ML}{\mbox{\isa{\isatt{{\isachartilde}{\isachartilde}{\isacharslash}src{\isacharslash}Pure{\isacharslash}Concurrent{\isacharslash}mailbox{\isachardot}ML}}}} how to
+  implement a mailbox as synchronized variable over a purely
+  functional queue.
 
-  \smallskip\begin{mldecls}
-\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
-\verb|         (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
-\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
-\verb|       else Sign.declare_const|\isasep\isanewline%
-\verb|         ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
-
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Options and partiality%
-}
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{is\_some}\verb|is_some: 'a option -> bool| \\
-  \indexdef{}{ML}{is\_none}\verb|is_none: 'a option -> bool| \\
-  \indexdef{}{ML}{the}\verb|the: 'a option -> 'a| \\
-  \indexdef{}{ML}{these}\verb|these: 'a list option -> 'a list| \\
-  \indexdef{}{ML}{the\_list}\verb|the_list: 'a option -> 'a list| \\
-  \indexdef{}{ML}{the\_default}\verb|the_default: 'a -> 'a option -> 'a| \\
-  \indexdef{}{ML}{try}\verb|try: ('a -> 'b) -> 'a -> 'b option| \\
-  \indexdef{}{ML}{can}\verb|can: ('a -> 'b) -> 'a -> bool| \\
-  \end{mldecls}%
+  \medskip The following example implements a counter that produces
+  positive integers that are unique over the runtime of the Isabelle
+  process:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
+\endisatagmlex
+{\isafoldmlex}%
 %
-\begin{isamarkuptext}%
-Standard selector functions on \isa{option}s are provided.  The
-  \verb|try| and \verb|can| functions provide a convenient interface for
-  handling exceptions -- both take as arguments a function \verb|f|
-  together with a parameter \verb|x| and handle any exception during
-  the evaluation of the application of \verb|f| to \verb|x|, either
-  return a lifted result (\verb|NONE| on failure) or a boolean value
-  (\verb|false| on failure).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Common data structures%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists (as set-like data structures)%
-}
-\isamarkuptrue%
+\isadelimmlex
 %
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML}{member}\verb|member: ('b * 'a -> bool) -> 'a list -> 'b -> bool| \\
-  \indexdef{}{ML}{insert}\verb|insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list| \\
-  \indexdef{}{ML}{remove}\verb|remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list| \\
-  \indexdef{}{ML}{merge}\verb|merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list| \\
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimmlex
 %
-\begin{isamarkuptext}%
-Lists are often used as set-like data structures -- set-like in
-  the sense that they support a notion of \verb|member|-ship,
-  \verb|insert|-ing and \verb|remove|-ing, but are order-sensitive.
-  This is convenient when implementing a history-like mechanism:
-  \verb|insert| adds an element \emph{to the front} of a list,
-  if not yet present; \verb|remove| removes \emph{all} occurences
-  of a particular element.  Correspondingly \verb|merge| implements a 
-  a merge on two lists suitable for merges of context data
-  (\secref{sec:context-theory}).
-
-  Functions are parametrized by an explicit equality function
-  to accomplish overloaded equality;  in most cases of monomorphic
-  equality, writing \verb|op =| should suffice.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
 %
-\isamarkupsubsection{Association lists%
-}
-\isamarkuptrue%
+\endisadelimML
 %
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML exception}{AList.DUP}\verb|exception AList.DUP| \\
-  \indexdef{}{ML}{AList.lookup}\verb|AList.lookup: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option| \\
-  \indexdef{}{ML}{AList.defined}\verb|AList.defined: ('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool| \\
-  \indexdef{}{ML}{AList.update}\verb|AList.update: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexdef{}{ML}{AList.default}\verb|AList.default: ('a * 'a -> bool) -> ('a * 'b) -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexdef{}{ML}{AList.delete}\verb|AList.delete: ('a * 'b -> bool) -> 'a -> ('b * 'c) list -> ('b * 'c) list| \\
-  \indexdef{}{ML}{AList.map\_entry}\verb|AList.map_entry: ('a * 'b -> bool) -> 'a|\isasep\isanewline%
-\verb|    -> ('c -> 'c) -> ('b * 'c) list -> ('b * 'c) list| \\
-  \indexdef{}{ML}{AList.map\_default}\verb|AList.map_default: ('a * 'a -> bool) -> 'a * 'b -> ('b -> 'b)|\isasep\isanewline%
-\verb|    -> ('a * 'b) list -> ('a * 'b) list| \\
-  \indexdef{}{ML}{AList.join}\verb|AList.join: ('a * 'a -> bool) -> ('a -> 'b * 'b -> 'b) (*exception DUP*)|\isasep\isanewline%
-\verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)| \\
-  \indexdef{}{ML}{AList.merge}\verb|AList.merge: ('a * 'a -> bool) -> ('b * 'b -> bool)|\isasep\isanewline%
-\verb|    -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list (*exception AList.DUP*)|
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Association lists can be seens as an extension of set-like lists:
-  on the one hand, they may be used to implement finite mappings,
-  on the other hand, they remain order-sensitive and allow for
-  multiple key-value-pair with the same key: \verb|AList.lookup|
-  returns the \emph{first} value corresponding to a particular
-  key, if present.  \verb|AList.update| updates
-  the \emph{first} occurence of a particular key; if no such
-  key exists yet, the key-value-pair is added \emph{to the front}.
-  \verb|AList.delete| only deletes the \emph{first} occurence of a key.
-  \verb|AList.merge| provides an operation suitable for merges of context data
-  (\secref{sec:context-theory}), where an equality parameter on
-  values determines whether a merge should be considered a conflict.
-  A slightly generalized operation if implementend by the \verb|AList.join|
-  function which allows for explicit conflict resolution.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Tables%
-}
-\isamarkuptrue%
+\isatagML
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ local\isanewline
+\ \ \ \ val\ counter\ {\isacharequal}\ Synchronized{\isachardot}var\ {\isachardoublequote}counter{\isachardoublequote}\ {\isadigit{0}}{\isacharsemicolon}\isanewline
+\ \ in\isanewline
+\ \ \ \ fun\ next\ {\isacharparenleft}{\isacharparenright}\ {\isacharequal}\isanewline
+\ \ \ \ \ \ Synchronized{\isachardot}guarded{\isacharunderscore}access\ counter\isanewline
+\ \ \ \ \ \ \ \ {\isacharparenleft}fn\ i\ {\isacharequal}{\isachargreater}\isanewline
+\ \ \ \ \ \ \ \ \ \ let\ val\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isadigit{1}}\isanewline
+\ \ \ \ \ \ \ \ \ \ in\ SOME\ {\isacharparenleft}j{\isacharcomma}\ j{\isacharparenright}\ end{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ end{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}\isanewline
+\isanewline
+\isacommand{ML}\isamarkupfalse%
+\ {\isacharverbatimopen}\isanewline
+\ \ val\ a\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ val\ b\ {\isacharequal}\ next\ {\isacharparenleft}{\isacharparenright}{\isacharsemicolon}\isanewline
+\ \ %
+\isaantiq
+assert%
+\endisaantiq
+\ {\isacharparenleft}a\ {\isacharless}{\isachargreater}\ b{\isacharparenright}{\isacharsemicolon}\isanewline
+{\isacharverbatimclose}%
+\endisatagML
+{\isafoldML}%
 %
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML type}{'a Symtab.table}\verb|type 'a Symtab.table| \\
-  \indexdef{}{ML exception}{Symtab.DUP}\verb|exception Symtab.DUP of string| \\
-  \indexdef{}{ML exception}{Symtab.SAME}\verb|exception Symtab.SAME| \\
-  \indexdef{}{ML exception}{Symtab.UNDEF}\verb|exception Symtab.UNDEF of string| \\
-  \indexdef{}{ML}{Symtab.empty}\verb|Symtab.empty: 'a Symtab.table| \\
-  \indexdef{}{ML}{Symtab.lookup}\verb|Symtab.lookup: 'a Symtab.table -> string -> 'a option| \\
-  \indexdef{}{ML}{Symtab.defined}\verb|Symtab.defined: 'a Symtab.table -> string -> bool| \\
-  \indexdef{}{ML}{Symtab.update}\verb|Symtab.update: (string * 'a) -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexdef{}{ML}{Symtab.default}\verb|Symtab.default: string * 'a -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexdef{}{ML}{Symtab.delete}\verb|Symtab.delete: string|\isasep\isanewline%
-\verb|    -> 'a Symtab.table -> 'a Symtab.table (*exception Symtab.UNDEF*)| \\
-  \indexdef{}{ML}{Symtab.map\_entry}\verb|Symtab.map_entry: string -> ('a -> 'a)|\isasep\isanewline%
-\verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexdef{}{ML}{Symtab.map\_default}\verb|Symtab.map_default: (string * 'a) -> ('a -> 'a)|\isasep\isanewline%
-\verb|    -> 'a Symtab.table -> 'a Symtab.table| \\
-  \indexdef{}{ML}{Symtab.join}\verb|Symtab.join: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*)|\isasep\isanewline%
-\verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb|    -> 'a Symtab.table (*exception Symtab.DUP*)| \\
-  \indexdef{}{ML}{Symtab.merge}\verb|Symtab.merge: ('a * 'a -> bool)|\isasep\isanewline%
-\verb|    -> 'a Symtab.table * 'a Symtab.table|\isasep\isanewline%
-\verb|    -> 'a Symtab.table (*exception Symtab.DUP*)|
-  \end{mldecls}%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\isadelimML
 %
-\begin{isamarkuptext}%
-Tables are an efficient representation of finite mappings without
-  any notion of order;  due to their efficiency they should be used
-  whenever such pure finite mappings are neccessary.
-
-  The key type of tables must be given explicitly by instantiating
-  the \verb|Table| functor which takes the key type
-  together with its \verb|order|; for convience, we restrict
-  here to the \verb|Symtab| instance with \verb|string|
-  as key type.
-
-  Most table functions correspond to those of association lists.%
-\end{isamarkuptext}%
-\isamarkuptrue%
+\endisadelimML
+\isanewline
 %
 \isadelimtheory
+\isanewline
 %
 \endisadelimtheory
 %




