src/Doc/Implementation/ML.thy

 
   As in regular typography, there is some extra space \emph{before}
   section headings that are adjacent to plain text, but not other headings
   as in the example above.
 
-  \medskip The precise wording of the prose text given in these
+  \<^medskip>
+  The precise wording of the prose text given in these
   headings is chosen carefully to introduce the main theme of the
   subsequent formal ML text.
 \<close>
 
 

   \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 used for
   certain ML categories as follows:
 
-  \medskip
+  \<^medskip>
   \begin{tabular}{lll}
   variant & example & ML categories \\\hline
   lower-case & @{ML_text foo_bar} & values, types, record fields \\
   capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
   upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
   \end{tabular}
-  \medskip
+  \<^medskip>
 
   For historical reasons, many capitalized names omit underscores,
   e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
   Genuine mixed-case names are \emph{not} used, because clear division
   of words is essential for readability.\footnote{Camel-case was

   \paragraph{Specific conventions.} Here are some specific name forms
   that occur frequently in the sources.
 
   \begin{itemize}
 
-  \item A function that maps @{ML_text foo} to @{ML_text bar} is
+  \<^item> A function that maps @{ML_text foo} to @{ML_text bar} is
   called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
   @{ML_text foo2bar}, nor @{ML_text bar_from_foo}, nor @{ML_text
   bar_for_foo}, nor @{ML_text bar4foo}).
 
-  \item The name component @{ML_text legacy} means that the operation
+  \<^item> The name component @{ML_text legacy} means that the operation
   is about to be discontinued soon.
 
-  \item The name component @{ML_text global} means that this works
+  \<^item> The name component @{ML_text 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
+  \<^item> Variables of the main context types of the Isabelle/Isar
   framework (\secref{sec:context} and \chref{ch:local-theory}) have
   firm naming conventions as follows:
 
   \begin{itemize}
 
-  \item theories are called @{ML_text thy}, rarely @{ML_text theory}
+  \<^item> theories are called @{ML_text thy}, rarely @{ML_text theory}
   (never @{ML_text thry})
 
-  \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
+  \<^item> proof contexts are called @{ML_text ctxt}, rarely @{ML_text
   context} (never @{ML_text ctx})
 
-  \item generic contexts are called @{ML_text context}
-
-  \item local theories are called @{ML_text lthy}, except for local
+  \<^item> generic contexts are called @{ML_text context}
+
+  \<^item> local theories are called @{ML_text lthy}, except for local
   theories that are treated as proof context (which is a semantic
   super-type)
 
   \end{itemize}
 

   well as semantic prefixes like @{ML_text foo_thy} or @{ML_text
   bar_ctxt}, but the base conventions above need to be preserved.
   This allows to emphasize their data flow via plain regular
   expressions in the text editor.
 
-  \item The main logical entities (\secref{ch:logic}) have established
+  \<^item> The main logical entities (\secref{ch:logic}) have established
   naming convention as follows:
 
   \begin{itemize}
 
-  \item sorts are called @{ML_text S}
-
-  \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
+  \<^item> sorts are called @{ML_text S}
+
+  \<^item> types are called @{ML_text T}, @{ML_text U}, or @{ML_text
   ty} (never @{ML_text t})
 
-  \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
+  \<^item> terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
   tm} (never @{ML_text trm})
 
-  \item certified types are called @{ML_text cT}, rarely @{ML_text
+  \<^item> certified types are called @{ML_text cT}, rarely @{ML_text
   T}, with variants as for types
 
-  \item certified terms are called @{ML_text ct}, rarely @{ML_text
+  \<^item> certified terms are called @{ML_text ct}, rarely @{ML_text
   t}, with variants as for terms (never @{ML_text ctrm})
 
-  \item theorems are called @{ML_text th}, or @{ML_text thm}
+  \<^item> theorems are called @{ML_text th}, or @{ML_text 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

   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
+  \<^medskip>
+  For similar reasons, any kind of two-dimensional or tabular
   layouts, ASCII-art with lines or boxes of asterisks etc.\ should be
   avoided.
 
   \paragraph{Complex expressions} that consist of multi-clausal
   function definitions, @{ML_text handle}, @{ML_text case},

 
   Extra parentheses around @{ML_text case} expressions are optional,
   but help to analyse the nesting based on character matching in the
   text editor.
 
-  \medskip There are two main exceptions to the overall principle of
+  \<^medskip>
+  There are two main exceptions to the overall principle of
   compositionality in the layout of complex expressions.
 
   \begin{enumerate}
 
-  \item @{ML_text "if"} expressions are iterated as if ML had multi-branch
+  \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch
   conditionals, e.g.
 
   \begin{verbatim}
   (* RIGHT *)
 
   if b1 then e1
   else if b2 then e2
   else e3
   \end{verbatim}
 
-  \item @{ML_text fn} abstractions are often layed-out as if they
+  \<^enum> @{ML_text 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.  Example:
 
   \begin{verbatim}

       val y = ...
     in
       ... end
   \end{verbatim}
 
-  \medskip In general the source layout is meant to emphasize the
+  \<^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, Scala, Java).
 \<close>
 
 

   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, using
+  \<^medskip>
+  The next example shows how to embed ML into Isar proofs, using
   @{command_ref "ML_prf"} instead of @{command_ref "ML"}. As illustrated
   below, the effect on the ML environment is local to the whole proof body,
-  but ignoring the block structure. \<close>
+  but ignoring the block structure.\<close>
 
 notepad
 begin
   ML_prf %"ML" \<open>val a = 1\<close>
   {

 text \<open>By side-stepping the normal scoping rules for Isar proof
   blocks, embedded ML code can refer to the different contexts and
   manipulate corresponding entities, e.g.\ export a fact from a block
   context.
 
-  \medskip Two further ML commands are useful in certain situations:
+  \<^medskip>
+  Two further ML commands are useful in certain situations:
   @{command_ref ML_val} and @{command_ref ML_command} are \emph{diagnostic} in
   the sense that there is no effect on the underlying environment, and can
   thus be used anywhere. The examples below produce long strings of digits by
   invoking @{ML factorial}: @{command ML_val} takes care of printing the ML
   toplevel result, but @{command ML_command} is silent so we produce an

   \<close>}
 
   Here @{syntax nameref} and @{syntax args} are outer syntax categories, as
   defined in @{cite "isabelle-isar-ref"}.
 
-  \medskip A regular antiquotation @{text "@{name args}"} processes
+  \<^medskip>
+  A regular antiquotation @{text "@{name args}"} 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.\ @{text "@{term t}"}) or abstract
   \emph{value} (e.g. @{text "@{thm th}"}).  This pre-compilation
   scheme allows to refer to formal entities in a robust manner, with

   in their application.  In Isabelle/ML, large portions of text can be
   written without auxiliary operations like @{text "swap: \<alpha> \<times> \<beta> \<rightarrow> \<beta> \<times>
   \<alpha>"} or @{text "C: (\<alpha> \<rightarrow> \<beta> \<rightarrow> \<gamma>) \<rightarrow> (\<beta> \<rightarrow> \<alpha> \<rightarrow> \<gamma>)"} (the latter is not
   present in the Isabelle/ML library).
 
-  \medskip The main idea is that arguments that vary less are moved
+  \<^medskip>
+  The main 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

   becomes hard to read and maintain if the functions are themselves
   given as complex expressions.  The notation can be significantly
   improved by introducing \emph{forward} versions of application and
   composition as follows:
 
-  \medskip
+  \<^medskip>
   \begin{tabular}{lll}
   @{text "x |> f"} & @{text "\<equiv>"} & @{text "f x"} \\
   @{text "(f #> g) x"} & @{text "\<equiv>"} & @{text "x |> f |> g"} \\
   \end{tabular}
-  \medskip
+  \<^medskip>
 
   This enables to write conveniently @{text "x |> f\<^sub>1 |> \<dots> |> f\<^sub>n"} or
   @{text "f\<^sub>1 #> \<dots> #> f\<^sub>n"} for its functional abstraction over @{text
   "x"}.
 
-  \medskip There is an additional set of combinators to accommodate
+  \<^medskip>
+  There is an additional set of combinators to accommodate
   multiple results (via pairs) that are passed on as multiple
   arguments (via currying).
 
-  \medskip
+  \<^medskip>
   \begin{tabular}{lll}
   @{text "(x, y) |-> f"} & @{text "\<equiv>"} & @{text "f x y"} \\
   @{text "(f #-> g) x"} & @{text "\<equiv>"} & @{text "x |> f |-> g"} \\
   \end{tabular}
-  \medskip
+  \<^medskip>
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\

   an extra @{ML "map"} over the given list.  This kind of peephole
   optimization reduces both the code size and the tree structures in
   memory (``deforestation''), but it requires some practice to read
   and write fluently.
 
-  \medskip The next example elaborates the idea of canonical
+  \<^medskip>
+  The next example elaborates the idea of canonical
   iteration, demonstrating fast accumulation of tree content using a
   text buffer.
 \<close>
 
 ML \<open>

     "Beware the Jubjub Bird, and shun",
     "The frumious Bandersnatch!"]);
 \<close>
 
 text \<open>
-  \medskip An alternative is to make a paragraph of freely-floating words as
+  \<^medskip>
+  An alternative is to make a paragraph of freely-floating words as
   follows.
 \<close>
 
 ML_command \<open>
   warning (Pretty.string_of (Pretty.para

   Traditionally, the (short) exception message would include the name
   of an ML function, although this is no longer necessary, because the
   ML runtime system attaches detailed source position stemming from the
   corresponding @{ML_text raise} keyword.
 
-  \medskip User modules can always introduce their own custom
+  \<^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 users of a module
   can be often minimized by using plain user errors instead.

   in itself a small string, which has either one of the following
   forms:
 
   \begin{enumerate}
 
-  \item a single ASCII character ``@{text "c"}'', for example
+  \<^enum> a single ASCII character ``@{text "c"}'', for example
   ``@{verbatim a}'',
 
-  \item a codepoint according to UTF-8 (non-ASCII byte sequence),
-
-  \item a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}@{text
+  \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
+
+  \<^enum> a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}@{text
   "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<alpha>"}'',
 
-  \item a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}@{text
+  \<^enum> a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}@{text
   "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'',
 
-  \item a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}@{text
+  \<^enum> a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}@{text
   text}@{verbatim ">"}'' where @{text text} consists of printable characters
   excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example
   ``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'',
 
-  \item a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
+  \<^enum> a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
   "<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for
   example ``@{verbatim "\<^raw42>"}''.
 
   \end{enumerate}
 

   encoding is processed in a non-strict fashion, such that well-formed code
   sequences are recognized accordingly. Unicode provides its own collection of
   mathematical symbols, but within the core Isabelle/ML world there is no link
   to the standard collection of Isabelle regular symbols.
 
-  \medskip Output of Isabelle symbols depends on the print mode. For example,
+  \<^medskip>
+  Output of Isabelle symbols depends on the print mode. For example,
   the standard {\LaTeX} setup of the Isabelle document preparation system
   would present ``@{verbatim "\<alpha>"}'' as @{text "\<alpha>"}, and ``@{verbatim
   "\<^bold>\<alpha>"}'' as @{text "\<^bold>\<alpha>"}. On-screen rendering usually works by mapping a
   finite subset of Isabelle symbols to suitable Unicode characters.
 \<close>

   Isabelle-specific purposes with the following implicit substructures
   packed into the string content:
 
   \begin{enumerate}
 
-  \item sequence of Isabelle symbols (see also \secref{sec:symbols}),
+  \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}),
   with @{ML Symbol.explode} as key operation;
 
-  \item XML tree structure via YXML (see also @{cite "isabelle-system"}),
+  \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}),
   with @{ML YXML.parse_body} as key operation.
 
   \end{enumerate}
 
   Note that Isabelle/ML string literals may refer Isabelle symbols like

   @{cite "Wenzel:2009"}. This means, significant parts of theory and proof
   checking is parallelized by default. In Isabelle2013, a maximum
   speedup-factor of 3.5 on 4 cores and 6.5 on 8 cores can be expected
   @{cite "Wenzel:2013:ITP"}.
 
-  \medskip ML threads lack the memory protection of separate
+  \<^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 directly
   available to other threads: abstract values can be passed without
   copying or awkward serialization that is typically required for
   separate processes.

   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.\ mutable memory cells that
+  \<^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 Global state of the running Isabelle/ML process, i.e.\ raw I/O
+  \<^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
+  \<^item> Writable resources in the file-system that are shared among
   different threads or external processes.
 
   \end{itemize}
 
   Isabelle/ML provides various mechanisms to avoid critical shared

   help to make Isabelle/ML programs work smoothly in a concurrent
   environment.
 
   \begin{itemize}
 
-  \item Avoid global references altogether.  Isabelle/Isar maintains a
+  \<^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 historic reference variables.
 
-  \item Keep components with local state information re-entrant.
+  \<^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
   contain mutable references in special situations, without requiring any
   synchronization, as long as each invocation gets its own copy and the
   tool itself is single-threaded.
 
-  \item Avoid raw output on @{text "stdout"} or @{text "stderr"}.  The
+  \<^item> Avoid raw output on @{text "stdout"} or @{text "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.
 

   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
+  \<^item> Treat environment variables and the current working directory
   of the running process as read-only.
 
-  \item Restrict writing to the file-system to unique temporary files.
+  \<^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.

   val a = next ();
   val b = next ();
   @{assert} (a <> b);
 \<close>
 
-text \<open>\medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
+text \<open>
+  \<^medskip>
+  See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
   to implement a mailbox as synchronized variable over a purely
   functional list.\<close>
 
 
 section \<open>Managed evaluation\<close>

   specifically when and how evaluation happens.  For example, the
   Isabelle/ML library supports lazy evaluation with memoing, parallel
   evaluation via futures, asynchronous evaluation via promises,
   evaluation with time limit etc.
 
-  \medskip An \emph{unevaluated expression} is represented either as
+  \<^medskip>
+  An \emph{unevaluated expression} is represented either as
   unit abstraction @{verbatim "fn () => a"} of type
   @{verbatim "unit -> 'a"} or as regular function
   @{verbatim "fn a => b"} of type @{verbatim "'a -> 'b"}.  Both forms
   occur routinely, and special care is required to tell them apart ---
   the static type-system of SML is only of limited help here.

   some combinator @{text "('a -> 'b) -> 'a -> 'b"} acts like a
   modified form of function application; several such combinators may
   be cascaded to modify a given function, before it is ultimately
   applied to some argument.
 
-  \medskip \emph{Reified results} make the disjoint sum of regular
+  \<^medskip>
+  \emph{Reified results} make the disjoint sum of regular
   values versions exceptional situations explicit as ML datatype:
   @{text "'a result = Res of 'a | Exn of exn"}.  This is typically
   used for administrative purposes, to store the overall outcome of an
   evaluation process.
 

   wait operations), or if non-worker threads contend for significant runtime
   resources independently. There is a limited number of replacement worker
   threads that get activated in certain explicit wait conditions, after a
   timeout.
 
-  \medskip Each future task belongs to some \emph{task group}, which
+  \<^medskip>
+  Each future task belongs to some \emph{task group}, which
   represents the hierarchic structure of related tasks, together with the
   exception status a that point. By default, the task group of a newly created
   future is a new sub-group of the presently running one, but it is also
   possible to indicate different group layouts under program control.
 

   particular task group, its \emph{group status} cumulates all relevant
   exceptions according to its position within the group hierarchy. Interrupted
   tasks that lack regular result information, will pick up parallel exceptions
   from the cumulative group status.
 
-  \medskip A \emph{passive future} or \emph{promise} is a future with slightly
+  \<^medskip>
+  A \emph{passive future} or \emph{promise} is a future with slightly
   different evaluation policies: there is only a single-assignment variable
   and some expression to evaluate for the \emph{failed} case (e.g.\ to clean
   up resources when canceled). A regular result is produced by external means,
   using a separate \emph{fulfill} operation.
 

   fork several futures simultaneously. The @{text params} consist of the
   following fields:
 
   \begin{itemize}
 
-  \item @{text "name : string"} (default @{ML "\"\""}) specifies a common name
+  \<^item> @{text "name : string"} (default @{ML "\"\""}) specifies a common name
   for the tasks of the forked futures, which serves diagnostic purposes.
 
-  \item @{text "group : Future.group option"} (default @{ML NONE}) specifies
+  \<^item> @{text "group : Future.group option"} (default @{ML NONE}) specifies
   an optional task group for the forked futures. @{ML NONE} means that a new
   sub-group of the current worker-thread task context is created. If this is
   not a worker thread, the group will be a new root in the group hierarchy.
 
-  \item @{text "deps : Future.task list"} (default @{ML "[]"}) specifies
+  \<^item> @{text "deps : Future.task list"} (default @{ML "[]"}) specifies
   dependencies on other future tasks, i.e.\ the adjacency relation in the
   global task queue. Dependencies on already finished tasks are ignored.
 
-  \item @{text "pri : int"} (default @{ML 0}) specifies a priority within the
+  \<^item> @{text "pri : int"} (default @{ML 0}) specifies a priority within the
   task queue.
 
   Typically there is only little deviation from the default priority @{ML 0}.
   As a rule of thumb, @{ML "~1"} means ``low priority" and @{ML 1} means
   ``high priority''.

   thread priority. When a worker thread picks up a task for processing, it
   runs with the normal thread priority to the end (or until canceled). Higher
   priority tasks that are queued later need to wait until this (or another)
   worker thread becomes free again.
 
-  \item @{text "interrupts : bool"} (default @{ML true}) tells whether the
+  \<^item> @{text "interrupts : bool"} (default @{ML true}) tells whether the
   worker thread that processes the corresponding task is initially put into
   interruptible state. This state may change again while running, by modifying
   the thread attributes.
 
   With interrupts disabled, a running future task cannot be canceled.  It is