src/Doc/Implementation/ML.thy

 
   The rest of the file is divided into sections, subsections,
   subsubsections, paragraphs etc.\ using a simple layout via ML
   comments as follows.
 
-  \begin{verbatim}
-  (*** section ***)
+  @{verbatim [display]
+\<open>  (*** section ***)
 
   (** subsection **)
 
   (* subsubsection *)
 
   (*short paragraph*)
 
   (*
     long paragraph,
     with more text
-  *)
-  \end{verbatim}
+  *)\<close>}
 
   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.
 

   called @{ML_text helper}, @{ML_text aux}, or @{ML_text f} is
   considered bad style.
 
   Example:
 
-  \begin{verbatim}
-  (* RIGHT *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   fun print_foo ctxt foo =
     let
       fun print t = ... Syntax.string_of_term ctxt t ...
     in ... end;

   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}
+    in ... end;\<close>}
 
 
   \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
   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}).

   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}
-  (never @{ML_text thry})
-
-  \<^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
-  theories that are treated as proof context (which is a semantic
-  super-type)
+    \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
+    context} (never @{ML_text ctx})
+
+    \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}
 
   Variations with primed or decimal numbers are always possible, as
   well as semantic prefixes like @{ML_text foo_thy} or @{ML_text

   \<^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
-  ty} (never @{ML_text t})
-
-  \<^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
-  T}, with variants as for types
-
-  \<^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 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
+    tm} (never @{ML_text trm})
+
+    \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
+    t}, with variants as for terms (never @{ML_text ctrm})
+
+    \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

   (if made explicit) is usually called @{ML_text st} instead of the
   somewhat misleading @{ML_text thm}.  Any other arguments are given
   before the latter two, and the general context is given first.
   Example:
 
-  \begin{verbatim}
-  fun my_tac ctxt arg1 arg2 i st = ...
-  \end{verbatim}
+  @{verbatim [display] \<open>  fun my_tac ctxt arg1 arg2 i st = ...\<close>}
 
   Note that the goal state @{ML_text st} above is rarely made
   explicit, if tactic combinators (tacticals) are used as usual.
 
   A tactic that requires a proof context needs to make that explicit as seen
   in the @{verbatim ctxt} argument above. Do not refer to the background
   theory of @{verbatim st} -- it is not a proper context, but merely a formal
   certificate.
-
-  \end{itemize}
 \<close>
 
 
 subsection \<open>General source layout\<close>
 

   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);
+  @{verbatim [display]
+\<open>  val x = y + z * (a + b);
   val pair = (a, b);
-  val record = {foo = 1, bar = 2};
-  \end{verbatim}
+  val record = {foo = 1, bar = 2};\<close>}
 
   Lines are normally broken \emph{after} an infix operator or
   punctuation character.  For example:
 
-  \begin{verbatim}
+  @{verbatim [display]
+\<open>
   val x =
     a +
     b +
     c;
 
   val tuple =
    (a,
     b,
     c);
-  \end{verbatim}
+\<close>}
 
   Some special infixes (e.g.\ @{ML_text "|>"}) work better at the
   start of the line, but punctuation is always at the end.
 
   Function application follows the tradition of @{text "\<lambda>"}-calculus,

 
   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 *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   if b then
     expr1_part1
     expr1_part2
   else

   (* WRONG *)
 
   if b then expr1_part1
             expr1_part2
   else expr2_part1
-       expr2_part2
-  \end{verbatim}
+       expr2_part2\<close>}
 
   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

 
   Multiple clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
   @{ML_text case} get extra indentation to indicate the nesting
   clearly.  Example:
 
-  \begin{verbatim}
-  (* RIGHT *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   fun foo p1 =
         expr1
     | foo p2 =
         expr2

   (* WRONG *)
 
   fun foo p1 =
     expr1
     | foo p2 =
-    expr2
-  \end{verbatim}
+    expr2\<close>}
 
   Body expressions consisting of @{ML_text case} or @{ML_text let}
   require care to maintain compositionality, to prevent loss of
   logical indentation where it is especially important to see the
   structure of the text.  Example:
 
-  \begin{verbatim}
-  (* RIGHT *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   fun foo p1 =
         (case e of
           q1 => ...
         | q2 => ...)

     | foo p2 =
     let
       ...
     in
       ...
-    end
-  \end{verbatim}
+    end\<close>}
 
   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
   compositionality in the layout of complex expressions.
 
-  \begin{enumerate}
-
   \<^enum> @{ML_text "if"} expressions are iterated as if ML had multi-branch
   conditionals, e.g.
 
-  \begin{verbatim}
-  (* RIGHT *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   if b1 then e1
   else if b2 then e2
-  else e3
-  \end{verbatim}
+  else e3\<close>}
 
   \<^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}
-  (* RIGHT *)
+  @{verbatim [display]
+\<open>  (* RIGHT *)
 
   fun foo x y = fold (fn z =>
-    expr)
-  \end{verbatim}
+    expr)\<close>}
 
   Here the visual appearance is that of three arguments @{ML_text x},
   @{ML_text y}, @{ML_text z} in a row.
 
-  \end{enumerate}
 
   Such weakly structured layout should be use with great care.  Here
   are some counter-examples involving @{ML_text let} expressions:
 
-  \begin{verbatim}
-  (* WRONG *)
+  @{verbatim [display]
+\<open>  (* WRONG *)
 
   fun foo x = let
       val y = ...
     in ... end
 

 
   fun foo x =
     let
       val y = ...
     in
-      ... end
-  \end{verbatim}
+      ... end\<close>}
 
   \<^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).

   @{index_ML "Context.>>": "(Context.generic -> Context.generic) -> unit"} \\
   @{index_ML ML_Thms.bind_thms: "string * thm list -> unit"} \\
   @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML "ML_Context.the_generic_context ()"} refers to the theory
   context of the ML toplevel --- at compile time.  ML code needs to
   take care to refer to @{ML "ML_Context.the_generic_context ()"}
   correctly.  Recall that evaluation of a function body is delayed
   until actual run-time.

   ML toplevel, associating it with the provided name.
 
   \<^descr> @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but
   refers to a singleton fact.
 
-  \end{description}
 
   It is 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

   @@{ML_antiquotation make_string}
   ;
   @@{ML_antiquotation print} @{syntax name}?
   \<close>}
 
-  \begin{description}
-
   \<^descr> @{text "@{make_string}"} inlines a function to print arbitrary values
   similar to the ML toplevel. The result is compiler dependent and may fall
   back on "?" in certain situations. The value of configuration option
   @{attribute_ref ML_print_depth} determines further details of output.
 
   \<^descr> @{text "@{print f}"} uses the ML function @{text "f: string ->
   unit"} to output the result of @{text "@{make_string}"} above,
   together with the source position of the antiquotation.  The default
   output function is @{ML writeln}.
-
-  \end{description}
 \<close>
 
 text %mlex \<open>The following artificial examples show how to produce
   adhoc output of ML values for debugging purposes.\<close>
 

   @{index_ML fold: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   @{index_ML fold_rev: "('a -> 'b -> 'b) -> 'a list -> 'b -> 'b"} \\
   @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML fold}~@{text f} lifts the parametrized update function
   @{text "f"} to a list of parameters.
 
   \<^descr> @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text
   "f"}, but works inside-out, as if the list would be reversed.
 
   \<^descr> @{ML fold_map}~@{text "f"} lifts the parametrized update
   function @{text "f"} (with side-result) to a list of parameters and
   cumulative side-results.
 
-  \end{description}
 
   \begin{warn}
   The literature on functional programming provides a confusing multitude of
   combinators called @{text "foldl"}, @{text "foldr"} etc. SML97 provides its
   own variations as @{ML List.foldl} and @{ML List.foldr}, while the classic

   @{index_ML tracing: "string -> unit"} \\
   @{index_ML warning: "string -> unit"} \\
   @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML writeln}~@{text "text"} outputs @{text "text"} as regular
   message.  This is the primary message output operation of Isabelle
   and should be used by default.
 
   \<^descr> @{ML tracing}~@{text "text"} outputs @{text "text"} as special

   \begin{warn}
   The actual error channel is accessed via @{ML Output.error_message}, but
   this is normally not used directly in user code.
   \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 @{ML TextIO.output}) is apt to cause problems in

   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML try}~@{text "f x"} makes the partiality of evaluating
   @{text "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 @{ML_text "(SOME"}~@{text "f
   x"}~@{ML_text "handle _ => NONE)"} that is occasionally seen in

   a full trace of its stack of nested exceptions (if possible,
   depending on the ML platform).
 
   Inserting @{ML Runtime.exn_trace} into ML code temporarily is
   useful for debugging, but not suitable for production code.
-
-  \end{description}
 \<close>
 
 text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{description}
-
   \<^descr> @{text "@{assert}"} inlines a function
   @{ML_type "bool -> unit"} that raises @{ML Fail} if the argument is
   @{ML false}.  Due to inlining the source position of failed
   assertions is included in the error output.
-
-  \end{description}
 \<close>
 
 
 section \<open>Strings of symbols \label{sec:symbols}\<close>
 

   all.  Isabelle strings consist of a sequence of symbols, represented
   as a packed string or an exploded list of strings.  Each symbol is
   in itself a small string, which has either one of the following
   forms:
 
-  \begin{enumerate}
-
   \<^enum> a single ASCII character ``@{text "c"}'', for example
   ``@{verbatim a}'',
 
   \<^enum> a codepoint according to UTF-8 (non-ASCII byte sequence),
 

 
   \<^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}
 
   The @{text "ident"} syntax for symbol names is @{text "letter
   (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and @{text
   "digit = 0..9"}.  There are infinitely many regular symbols and
   control symbols, but a fixed collection of standard symbols is

   \begin{mldecls}
   @{index_ML_type "Symbol.sym"} \\
   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type "Symbol.symbol"} represents individual Isabelle
   symbols.
 
   \<^descr> @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
   from the packed form.  This function supersedes @{ML

   @{ML "Symbol.Malformed"}.
 
   \<^descr> @{ML "Symbol.decode"} converts the string representation of a
   symbol into the datatype version.
 
-  \end{description}
 
   \paragraph{Historical note.} In the original SML90 standard the
   primitive ML type @{ML_type char} did not exists, and @{ML_text
   "explode: string -> string list"} produced a list of singleton
   strings like @{ML "raw_explode: string -> string list"} in

 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type char} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type char} is \emph{not} used.  The smallest textual
   unit in Isabelle is represented as a ``symbol'' (see
   \secref{sec:symbols}).
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Strings\<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type string} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type string} represents immutable vectors of 8-bit
   characters.  There are operations in SML to convert back and forth
   to actual byte vectors, which are seldom used.
 
   This historically important raw text representation is used for
   Isabelle-specific purposes with the following implicit substructures
   packed into the string content:
 
   \begin{enumerate}
 
-  \<^enum> sequence of Isabelle symbols (see also \secref{sec:symbols}),
-  with @{ML Symbol.explode} as key operation;
-
-  \<^enum> XML tree structure via YXML (see also @{cite "isabelle-system"}),
-  with @{ML YXML.parse_body} as key operation.
-
+    \item 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"}),
+    with @{ML YXML.parse_body} as key operation.
+  
   \end{enumerate}
 
   Note that Isabelle/ML string literals may refer Isabelle symbols like
   ``@{verbatim \<alpha>}'' natively, \emph{without} escaping the backslash. This is a
   consequence of Isabelle treating all source text as strings of symbols,
   instead of raw characters.
-
-  \end{description}
 \<close>
 
 text %mlex \<open>The subsequent example illustrates the difference of
   physical addressing of bytes versus logical addressing of symbols in
   Isabelle strings.

 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type int} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type int} represents regular mathematical integers, which
   are \emph{unbounded}. Overflow is treated properly, but should never happen
   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).

 
   Structure @{ML_structure IntInf} of SML97 is obsolete and superseded by
   @{ML_structure Int}.  Structure @{ML_structure Integer} in @{file
   "~~/src/Pure/General/integer.ML"} provides some additional
   operations.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Time\<close>
 

   \begin{mldecls}
   @{index_ML_type Time.time} \\
   @{index_ML seconds: "real -> Time.time"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type Time.time} represents time abstractly according
   to the SML97 basis library definition.  This is adequate for
   internal ML operations, but awkward in concrete time specifications.
 
   \<^descr> @{ML seconds}~@{text "s"} turns the concrete scalar @{text
   "s"} (measured in seconds) into an abstract time value.  Floating
   point numbers are easy to use as configuration options in the
   context (see \secref{sec:config-options}) or system options that
   are maintained externally.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Options\<close>
 

   @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\
   @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML cons}~@{text "x xs"} evaluates to @{text "x :: xs"}.
 
   Tupled infix operators are a historical accident in Standard ML.
   The curried @{ML cons} amends this, but it should be only used when
   partial application is required.

   already a @{ML member} of the list, while @{ML update} ensures that
   the latest 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: later declarations take precedence over earlier ones.
-
-  \end{description}
 \<close>
 
 text %mlex \<open>Using canonical @{ML fold} together with @{ML cons} (or
   similar standard operations) alternates the orientation of data.
   The is quite natural and should not be altered forcible by inserting

   @{index_ML AList.lookup: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> 'c option"} \\
   @{index_ML AList.defined: "('a * 'b -> bool) -> ('b * 'c) list -> 'a -> bool"} \\
   @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update}
   implement the main ``framework operations'' for mappings in
   Isabelle/ML, following standard conventions for their names and
   types.
 

   The @{text "defined"} operation is essentially a contraction of @{ML
   is_some} and @{verbatim "lookup"}, but this is sufficiently frequent to
   justify its independent existence.  This also gives the
   implementation some opportunity for peep-hole optimization.
 
-  \end{description}
 
   Association lists are adequate as simple implementation of finite mappings
   in many practical situations. A more advanced table structure is defined in
   @{file "~~/src/Pure/General/table.ML"}; that version scales easily to
   thousands or millions of elements.

 
 text \<open>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.\ 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.}
 

   channels, environment variables, current working directory.
 
   \<^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
   resources in most 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> 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

   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}
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML File.tmp_path: "Path.T -> Path.T"} \\
   @{index_ML serial_string: "unit -> string"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML File.tmp_path}~@{text "path"} relocates the base
   component of @{text "path"} into the unique temporary directory of
   the running Isabelle/ML process.
 
   \<^descr> @{ML serial_string}~@{text "()"} creates a new serial number
   that is unique over the runtime of the Isabelle/ML process.
-
-  \end{description}
 \<close>
 
 text %mlex \<open>The following example shows how to create unique
   temporary file names.
 \<close>

   @{index_ML_type "'a Synchronized.var"} \\
   @{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
   @{index_ML Synchronized.guarded_access: "'a Synchronized.var ->
   ('a -> ('b * 'a) option) -> 'b"} \\
   \end{mldecls}
-
-  \begin{description}
 
   \<^descr> Type @{ML_type "'a Synchronized.var"} represents synchronized
   variables with state of type @{ML_type 'a}.
 
   \<^descr> @{ML Synchronized.var}~@{text "name x"} creates a synchronized

   manner; if @{text "f x"} produces @{ML SOME}~@{text "(y, x')"} it is
   satisfied and assigns the new state value @{text "x'"}, broadcasts a
   signal to all waiting threads on the associated condition variable,
   and returns the result @{text "y"}.
 
-  \end{description}
 
   There are some further variants of the @{ML
   Synchronized.guarded_access} combinator, see @{file
   "~~/src/Pure/Concurrent/synchronized.ML"} for details.
 \<close>

   @{index_ML Exn.release: "'a Exn.result -> 'a"} \\
   @{index_ML Par_Exn.release_all: "'a Exn.result list -> 'a list"} \\
   @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type "'a Exn.result"} represents the disjoint sum of
   ML results explicitly, with constructor @{ML Exn.Res} for regular
   values and @{ML "Exn.Exn"} for exceptions.
 
   \<^descr> @{ML Exn.capture}~@{text "f x"} manages the evaluation of

   \<^descr> @{ML Par_Exn.release_first} is similar to @{ML
   Par_Exn.release_all}, but only the first (meaningful) exception that has
   occurred in the original evaluation process is raised again, the others are
   ignored.  That single exception may get handled by conventional
   means in ML.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Parallel skeletons \label{sec:parlist}\<close>
 

   \begin{mldecls}
   @{index_ML Par_List.map: "('a -> 'b) -> 'a list -> 'b list"} \\
   @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> @{ML Par_List.map}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} is like @{ML
   "map"}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"}, but the evaluation of @{text "f x\<^sub>i"}
   for @{text "i = 1, \<dots>, n"} is performed in parallel.
 
   An exception in any @{text "f x\<^sub>i"} cancels the overall evaluation

   Par_List.map}.
 
   This generic parallel choice combinator is the basis for derived
   forms, such as @{ML Par_List.find_some}, @{ML Par_List.exists}, @{ML
   Par_List.forall}.
-
-  \end{description}
 \<close>
 
 text %mlex \<open>Subsequently, the Ackermann function is evaluated in
   parallel for some ranges of arguments.\<close>
 

   @{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
   @{index_ML Lazy.value: "'a -> 'a lazy"} \\
   @{index_ML Lazy.force: "'a lazy -> 'a"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim
   "'a"}.
 
   \<^descr> @{ML Lazy.lazy}~@{text "(fn () => e)"} wraps the unevaluated
   expression @{text e} as unfinished lazy value.

   lazy values.
 
   \<^descr> @{ML Lazy.force}~@{text x} produces the result of the lazy value in a
   thread-safe manner as explained above. Thus it may cause the current thread
   to wait on a pending evaluation attempt by another thread.
-
-  \end{description}
 \<close>
 
 
 subsection \<open>Futures \label{sec:futures}\<close>
 

   @{index_ML Future.cancel_group: "Future.group -> unit"} \\[0.5ex]
   @{index_ML Future.promise: "(unit -> unit) -> 'a future"} \\
   @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
   \end{mldecls}
 
-  \begin{description}
-
   \<^descr> Type @{ML_type "'a future"} represents future values over type
   @{verbatim "'a"}.
 
   \<^descr> @{ML Future.fork}~@{text "(fn () => e)"} registers the unevaluated
   expression @{text e} as unfinished future value, to be evaluated eventually

   fork several futures simultaneously. The @{text params} consist of the
   following fields:
 
   \begin{itemize}
 
-  \<^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
-  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
-  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
-  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''.
-
-  Note that the task priority only affects the position in the queue, not the
-  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
-  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
-  the responsibility of the programmer that this special state is retained
-  only briefly.
+    \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
+    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
+    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
+    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''.
+
+    Note that the task priority only affects the position in the queue, not the
+    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
+    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
+    the responsibility of the programmer that this special state is retained
+    only briefly.
 
   \end{itemize}
 
   \<^descr> @{ML Future.join}~@{text x} retrieves the value of an already finished
   future, which may lead to an exception, according to the result of its

   canceled.
 
   \<^descr> @{ML Future.fulfill}~@{text "x a"} finishes the passive future @{text
   x} by the given value @{text a}. If the promise has already been canceled,
   the attempt to fulfill it causes an exception.
-
-  \end{description}
 \<close>
 
 end