src/Doc/Implementation/ML.thy

   Proper semantic names override these conventions completely.  For
   example, the left-hand side of an equation (as a term) can be called
   @{ML_text lhs} (not @{ML_text lhs_tm}).  Or a term that is known
   to be a variable can be called @{ML_text v} or @{ML_text x}.
 
-  \item Tactics (\secref{sec:tactics}) are sufficiently important to
+  \<^item> Tactics (\secref{sec:tactics}) are sufficiently important to
   have specific naming conventions.  The name of a basic tactic
   definition always has a @{ML_text "_tac"} suffix, the subgoal index
   (if applicable) is always called @{ML_text i}, and the goal state
   (if made explicit) is usually called @{ML_text st} instead of the
   somewhat misleading @{ML_text thm}.  Any other arguments are given

   @{index_ML ML_Thms.bind_thm: "string * thm -> unit"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML "ML_Context.the_generic_context ()"} refers to the theory
+  \<^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.
 
-  \item @{ML "Context.>>"}~@{text f} applies context transformation
+  \<^descr> @{ML "Context.>>"}~@{text f} applies context transformation
   @{text f} to the implicit context of the ML toplevel.
 
-  \item @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
+  \<^descr> @{ML ML_Thms.bind_thms}~@{text "(name, thms)"} stores a list of
   theorems produced in ML both in the (global) theory context and the
   ML toplevel, associating it with the provided name.
 
-  \item @{ML ML_Thms.bind_thm} is similar to @{ML ML_Thms.bind_thms} but
+  \<^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

   @@{ML_antiquotation print} @{syntax name}?
   \<close>}
 
   \begin{description}
 
-  \item @{text "@{make_string}"} inlines a function to print arbitrary values
+  \<^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.
 
-  \item @{text "@{print f}"} uses the ML function @{text "f: string ->
+  \<^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}

   @{index_ML fold_map: "('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML fold}~@{text f} lifts the parametrized update function
+  \<^descr> @{ML fold}~@{text f} lifts the parametrized update function
   @{text "f"} to a list of parameters.
 
-  \item @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text
+  \<^descr> @{ML fold_rev}~@{text "f"} is similar to @{ML fold}~@{text
   "f"}, but works inside-out, as if the list would be reversed.
 
-  \item @{ML fold_map}~@{text "f"} lifts the parametrized update
+  \<^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}
 

   @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML writeln}~@{text "text"} outputs @{text "text"} as regular
+  \<^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.
 
-  \item @{ML tracing}~@{text "text"} outputs @{text "text"} as special
+  \<^descr> @{ML tracing}~@{text "text"} outputs @{text "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 @{ML warning}~@{text "text"} outputs @{text "text"} as
+  \<^descr> @{ML warning}~@{text "text"} outputs @{text "text"} as
   warning, which typically means some extra emphasis on the front-end
   side (color highlighting, icons, etc.).
 
-  \item @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text
+  \<^descr> @{ML error}~@{text "text"} raises exception @{ML ERROR}~@{text
   "text"} and thus lets the Isar toplevel print @{text "text"} on the
   error channel, which typically means some extra emphasis on the
   front-end side (color highlighting, icons, etc.).
 
   This assumes that the exception is not handled before the command

   @{index_ML Runtime.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML try}~@{text "f x"} makes the partiality of evaluating
+  \<^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
   books about SML97, but not in Isabelle/ML.
 
-  \item @{ML can} is similar to @{ML try} with more abstract result.
-
-  \item @{ML ERROR}~@{text "msg"} represents user errors; this
+  \<^descr> @{ML can} is similar to @{ML try} with more abstract result.
+
+  \<^descr> @{ML ERROR}~@{text "msg"} represents user errors; this
   exception is normally raised indirectly via the @{ML error} function
   (see \secref{sec:message-channels}).
 
-  \item @{ML Fail}~@{text "msg"} represents general program failures.
-
-  \item @{ML Exn.is_interrupt} identifies interrupts robustly, without
+  \<^descr> @{ML Fail}~@{text "msg"} represents general program failures.
+
+  \<^descr> @{ML Exn.is_interrupt} identifies interrupts robustly, without
   mentioning concrete exception constructors in user code.  Handled
   interrupts need to be re-raised promptly!
 
-  \item @{ML reraise}~@{text "exn"} raises exception @{text "exn"}
+  \<^descr> @{ML reraise}~@{text "exn"} raises exception @{text "exn"}
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
+  \<^descr> @{ML Runtime.exn_trace}~@{ML_text "(fn () =>"}~@{text
   "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
   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

   @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   \begin{description}
 
-  \item @{text "@{assert}"} inlines a function
+  \<^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}

   @{index_ML Symbol.decode: "Symbol.symbol -> Symbol.sym"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type "Symbol.symbol"} represents individual Isabelle
+  \<^descr> Type @{ML_type "Symbol.symbol"} represents individual Isabelle
   symbols.
 
-  \item @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
+  \<^descr> @{ML "Symbol.explode"}~@{text "str"} produces a symbol list
   from the packed form.  This function supersedes @{ML
   "String.explode"} for virtually all purposes of manipulating text in
   Isabelle!\footnote{The runtime overhead for exploded strings is
   mainly that of the list structure: individual symbols that happen to
   be a singleton string do not require extra memory in Poly/ML.}
 
-  \item @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
+  \<^descr> @{ML "Symbol.is_letter"}, @{ML "Symbol.is_digit"}, @{ML
   "Symbol.is_quasi"}, @{ML "Symbol.is_blank"} classify standard
   symbols according to fixed syntactic conventions of Isabelle, cf.\
   @{cite "isabelle-isar-ref"}.
 
-  \item Type @{ML_type "Symbol.sym"} is a concrete datatype that
+  \<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that
   represents the different kinds of symbols explicitly, with
   constructors @{ML "Symbol.Char"}, @{ML "Symbol.UTF8"},
   @{ML "Symbol.Sym"}, @{ML "Symbol.Ctrl"}, @{ML "Symbol.Raw"},
   @{ML "Symbol.Malformed"}.
 
-  \item @{ML "Symbol.decode"} converts the string representation of a
+  \<^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

   @{index_ML_type char} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type char} is \emph{not} used.  The smallest textual
+  \<^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>

   @{index_ML_type string} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type string} represents immutable vectors of 8-bit
+  \<^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

   @{index_ML_type int} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type int} represents regular mathematical integers, which
+  \<^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).
 

   @{index_ML seconds: "real -> Time.time"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type Time.time} represents time abstractly according
+  \<^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.
 
-  \item @{ML seconds}~@{text "s"} turns the concrete scalar @{text
+  \<^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.
 

   @{index_ML update: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML cons}~@{text "x xs"} evaluates to @{text "x :: xs"}.
+  \<^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.
 
-  \item @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat
+  \<^descr> @{ML member}, @{ML insert}, @{ML remove}, @{ML update} treat
   lists as a set-like container that maintains the order of elements.
   See @{file "~~/src/Pure/library.ML"} for the full specifications
   (written in ML).  There are some further derived operations like
   @{ML union} or @{ML inter}.
 

   @{index_ML AList.update: "('a * 'a -> bool) -> 'a * 'b -> ('a * 'b) list -> ('a * 'b) list"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML AList.lookup}, @{ML AList.defined}, @{ML AList.update}
+  \<^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.
 
   Note that a function called @{verbatim lookup} is obliged to express its

   @{index_ML serial_string: "unit -> string"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML File.tmp_path}~@{text "path"} relocates the base
+  \<^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.
 
-  \item @{ML serial_string}~@{text "()"} creates a new serial number
+  \<^descr> @{ML serial_string}~@{text "()"} creates a new serial number
   that is unique over the runtime of the Isabelle/ML process.
 
   \end{description}
 \<close>
 

   ('a -> ('b * 'a) option) -> 'b"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type "'a Synchronized.var"} represents synchronized
+  \<^descr> Type @{ML_type "'a Synchronized.var"} represents synchronized
   variables with state of type @{ML_type 'a}.
 
-  \item @{ML Synchronized.var}~@{text "name x"} creates a synchronized
+  \<^descr> @{ML Synchronized.var}~@{text "name x"} creates a synchronized
   variable that is initialized with value @{text "x"}.  The @{text
   "name"} is used for tracing.
 
-  \item @{ML Synchronized.guarded_access}~@{text "var f"} lets the
+  \<^descr> @{ML Synchronized.guarded_access}~@{text "var f"} lets the
   function @{text "f"} operate within a critical section on the state
   @{text "x"} as follows: if @{text "f x"} produces @{ML NONE}, it
   continues to wait on the internal condition variable, expecting that
   some other thread will eventually change the content in a suitable
   manner; if @{text "f x"} produces @{ML SOME}~@{text "(y, x')"} it is

   @{index_ML Par_Exn.release_first: "'a Exn.result list -> 'a list"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type "'a Exn.result"} represents the disjoint sum of
+  \<^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.
 
-  \item @{ML Exn.capture}~@{text "f x"} manages the evaluation of
+  \<^descr> @{ML Exn.capture}~@{text "f x"} manages the evaluation of
   @{text "f x"} such that exceptions are made explicit as @{ML
   "Exn.Exn"}.  Note that this includes physical interrupts (see also
   \secref{sec:exceptions}), so the same precautions apply to user
   code: interrupts must not be absorbed accidentally!
 
-  \item @{ML Exn.interruptible_capture} is similar to @{ML
+  \<^descr> @{ML Exn.interruptible_capture} is similar to @{ML
   Exn.capture}, but interrupts are immediately re-raised as required
   for user code.
 
-  \item @{ML Exn.release}~@{text "result"} releases the original
+  \<^descr> @{ML Exn.release}~@{text "result"} releases the original
   runtime result, exposing its regular value or raising the reified
   exception.
 
-  \item @{ML Par_Exn.release_all}~@{text "results"} combines results
+  \<^descr> @{ML Par_Exn.release_all}~@{text "results"} combines results
   that were produced independently (e.g.\ by parallel evaluation).  If
   all results are regular values, that list is returned.  Otherwise,
   the collection of all exceptions is raised, wrapped-up as collective
   parallel exception.  Note that the latter prevents access to
   individual exceptions by conventional @{verbatim "handle"} of ML.
 
-  \item @{ML Par_Exn.release_first} is similar to @{ML
+  \<^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.
 

   @{index_ML Par_List.get_some: "('a -> 'b option) -> 'a list -> 'b option"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML Par_List.map}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} is like @{ML
+  \<^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
   process.  The final result is produced via @{ML
   Par_Exn.release_first} as explained above, which means the first
   program exception that happened to occur in the parallel evaluation
   is propagated, and all other failures are ignored.
 
-  \item @{ML Par_List.get_some}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} produces some
+  \<^descr> @{ML Par_List.get_some}~@{text "f [x\<^sub>1, \<dots>, x\<^sub>n]"} produces some
   @{text "f x\<^sub>i"} that is of the form @{text "SOME y\<^sub>i"}, if that
   exists, otherwise @{text "NONE"}.  Thus it is similar to @{ML
   Library.get_first}, but subject to a non-deterministic parallel
   choice process.  The first successful result cancels the overall
   evaluation process; other exceptions are propagated as for @{ML

   @{index_ML Lazy.force: "'a lazy -> 'a"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim
+  \<^descr> Type @{ML_type "'a lazy"} represents lazy values over type @{verbatim
   "'a"}.
 
-  \item @{ML Lazy.lazy}~@{text "(fn () => e)"} wraps the unevaluated
+  \<^descr> @{ML Lazy.lazy}~@{text "(fn () => e)"} wraps the unevaluated
   expression @{text e} as unfinished lazy value.
 
-  \item @{ML Lazy.value}~@{text a} wraps the value @{text a} as finished lazy
+  \<^descr> @{ML Lazy.value}~@{text a} wraps the value @{text a} as finished lazy
   value.  When forced, it returns @{text a} without any further evaluation.
 
   There is very low overhead for this proforma wrapping of strict values as
   lazy values.
 
-  \item @{ML Lazy.force}~@{text x} produces the result of the lazy value in a
+  \<^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>

   @{index_ML Future.fulfill: "'a future -> 'a -> unit"} \\
   \end{mldecls}
 
   \begin{description}
 
-  \item Type @{ML_type "'a future"} represents future values over type
+  \<^descr> Type @{ML_type "'a future"} represents future values over type
   @{verbatim "'a"}.
 
-  \item @{ML Future.fork}~@{text "(fn () => e)"} registers the unevaluated
+  \<^descr> @{ML Future.fork}~@{text "(fn () => e)"} registers the unevaluated
   expression @{text e} as unfinished future value, to be evaluated eventually
   on the parallel worker-thread farm. This is a shorthand for @{ML
   Future.forks} below, with default parameters and a single expression.
 
-  \item @{ML Future.forks}~@{text "params exprs"} is the general interface to
+  \<^descr> @{ML Future.forks}~@{text "params exprs"} is the general interface to
   fork several futures simultaneously. The @{text params} consist of the
   following fields:
 
   \begin{itemize}
 

   the responsibility of the programmer that this special state is retained
   only briefly.
 
   \end{itemize}
 
-  \item @{ML Future.join}~@{text x} retrieves the value of an already finished
+  \<^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
   previous evaluation.
 
   For an unfinished future there are several cases depending on the role of
   the current thread and the status of the future. A non-worker thread waits

 
   Whenever possible, static dependencies of futures should be specified
   explicitly when forked (see @{text deps} above). Thus the evaluation can
   work from the bottom up, without join conflicts and wait states.
 
-  \item @{ML Future.joins}~@{text xs} joins the given list of futures
+  \<^descr> @{ML Future.joins}~@{text xs} joins the given list of futures
   simultaneously, which is more efficient than @{ML "map Future.join"}~@{text
   xs}.
 
   Based on the dependency graph of tasks, the current thread takes over the
   responsibility to evaluate future expressions that are required for the main
   result, working from the bottom up. Waiting on future results that are
   presently evaluated on other threads only happens as last resort, when no
   other unfinished futures are left over.
 
-  \item @{ML Future.value}~@{text a} wraps the value @{text a} as finished
+  \<^descr> @{ML Future.value}~@{text a} wraps the value @{text a} as finished
   future value, bypassing the worker-thread farm. When joined, it returns
   @{text a} without any further evaluation.
 
   There is very low overhead for this proforma wrapping of strict values as
   futures.
 
-  \item @{ML Future.map}~@{text "f x"} is a fast-path implementation of @{ML
+  \<^descr> @{ML Future.map}~@{text "f x"} is a fast-path implementation of @{ML
   Future.fork}~@{text "(fn () => f ("}@{ML Future.join}~@{text "x))"}, which
   avoids the full overhead of the task queue and worker-thread farm as far as
   possible. The function @{text f} is supposed to be some trivial
   post-processing or projection of the future result.
 
-  \item @{ML Future.cancel}~@{text "x"} cancels the task group of the given
+  \<^descr> @{ML Future.cancel}~@{text "x"} cancels the task group of the given
   future, using @{ML Future.cancel_group} below.
 
-  \item @{ML Future.cancel_group}~@{text "group"} cancels all tasks of the
+  \<^descr> @{ML Future.cancel_group}~@{text "group"} cancels all tasks of the
   given task group for all time. Threads that are presently processing a task
   of the given group are interrupted: it may take some time until they are
   actually terminated. Tasks that are queued but not yet processed are
   dequeued and forced into interrupted state. Since the task group is itself
   invalidated, any further attempt to fork a future that belongs to it will
   yield a canceled result as well.
 
-  \item @{ML Future.promise}~@{text abort} registers a passive future with the
+  \<^descr> @{ML Future.promise}~@{text abort} registers a passive future with the
   given @{text abort} operation: it is invoked when the future task group is
   canceled.
 
-  \item @{ML Future.fulfill}~@{text "x a"} finishes the passive future @{text
+  \<^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>