src/Doc/Implementation/ML.thy

 
 theory "ML"
 imports Base
 begin
 
-chapter {* Isabelle/ML *}
-
-text {* Isabelle/ML is best understood as a certain culture based on
+chapter \<open>Isabelle/ML\<close>
+
+text \<open>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

   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.}  *}
-
-
-section {* Style and orthography *}
-
-text {* The sources of Isabelle/Isar are optimized for
+  merely reflect snapshots that are never really up-to-date.}\<close>
+
+
+section \<open>Style and orthography\<close>
+
+text \<open>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

 
   In a sense, good 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 code.
-*}
-
-
-subsection {* Header and sectioning *}
-
-text {* Isabelle source files have a certain standardized header
+\<close>
+
+
+subsection \<open>Header and sectioning\<close>
+
+text \<open>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.  See @{file "~~/src/Pure/thm.ML"}, for example.
 
   The header includes at least @{verbatim Title} and @{verbatim

   as in the example above.
 
   \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.
-*}
-
-
-subsection {* Naming conventions *}
-
-text {* Since ML is the primary medium to express the meaning of the
+\<close>
+
+
+subsection \<open>Naming conventions\<close>
+
+text \<open>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 used for

   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}
-*}
-
-
-subsection {* General source layout *}
-
-text {*
+\<close>
+
+
+subsection \<open>General source layout\<close>
+
+text \<open>
   The general Isabelle/ML source layout imitates regular type-setting
   conventions, augmented by the requirements for deeply nested expressions
   that are commonplace in functional programming.
 
   \paragraph{Line length} is limited to 80 characters according to ancient

   \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, Scala, Java).
-*}
-
-
-section {* ML embedded into Isabelle/Isar *}
-
-text {* ML and Isar are intertwined via an open-ended bootstrap
+\<close>
+
+
+section \<open>ML embedded into Isabelle/Isar\<close>
+
+text \<open>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).
 

   ".ML"} files that are loading from some theory. 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 standard repertoire of Isabelle, and there is no
   distinction between ``users'' and ``developers'' in this respect.
-*}
-
-
-subsection {* Isar ML commands *}
-
-text {*
+\<close>
+
+
+subsection \<open>Isar ML commands\<close>
+
+text \<open>
   The primary Isar source language provides facilities to ``open a window'' to
   the underlying ML compiler. Especially see the Isar commands @{command_ref
   "ML_file"} and @{command_ref "ML"}: both work the same way, but the source
   text is provided differently, 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 @{command_ref setup} or
   @{command_ref declaration}. Even more fine-grained embedding of ML into Isar
   is encountered in the proof method @{method_ref tactic}, which refines the
   pending goal state via a given expression of type @{ML_type tactic}.
-*}
-
-text %mlex {* The following artificial example demonstrates some ML
+\<close>
+
+text %mlex \<open>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.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   fun factorial 0 = 1
     | factorial n = n * factorial (n - 1)
-*}
-
-text {* Here the ML environment is already managed by Isabelle, i.e.\
+\<close>
+
+text \<open>Here the ML environment is already managed by Isabelle, i.e.\
   the @{ML 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

 
   \medskip The next example shows how to embed ML into Isar proofs, using
   @{command_ref "ML_prf"} instead of 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>
 
 notepad
 begin
-  ML_prf %"ML" {* val a = 1 *}
+  ML_prf %"ML" \<open>val a = 1\<close>
   {
-    ML_prf %"ML" {* val b = a + 1 *}
-  } -- {* Isar block structure ignored by ML environment *}
-  ML_prf %"ML" {* val c = b + 1 *}
+    ML_prf %"ML" \<open>val b = a + 1\<close>
+  } -- \<open>Isar block structure ignored by ML environment\<close>
+  ML_prf %"ML" \<open>val c = b + 1\<close>
 end
 
-text {* By side-stepping the normal scoping rules for Isar proof
+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:

   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
   explicit output message.
-*}
-
-ML_val {* factorial 100 *}
-ML_command {* writeln (string_of_int (factorial 100)) *}
+\<close>
+
+ML_val \<open>factorial 100\<close>
+ML_command \<open>writeln (string_of_int (factorial 100))\<close>
 
 notepad
 begin
-  ML_val {* factorial 100 *}
-  ML_command {* writeln (string_of_int (factorial 100)) *}
+  ML_val \<open>factorial 100\<close>
+  ML_command \<open>writeln (string_of_int (factorial 100))\<close>
 end
 
 
-subsection {* Compile-time context *}
-
-text {* Whenever the ML compiler is invoked within Isabelle/Isar, the
+subsection \<open>Compile-time context\<close>
+
+text \<open>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 done via some derived ML functions instead.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
   @{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"} \\

   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
   proof context at run-time, by explicit functional abstraction.
-*}
-
-
-subsection {* Antiquotations \label{sec:ML-antiq} *}
-
-text {* A very important consequence of embedding ML into Isar is the
+\<close>
+
+
+subsection \<open>Antiquotations \label{sec:ML-antiq}\<close>
+
+text \<open>A very important consequence of embedding ML into Isar is the
   concept of \emph{ML antiquotation}.  The standard token language of
   ML is augmented by special syntactic entities of the following form:
 
   @{rail \<open>
   @{syntax_def antiquote}: '@{' nameref args '}'

   \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
   proper static scoping and with some degree of logical checking of
   small portions of the code.
-*}
-
-
-subsection {* Printing ML values *}
-
-text {* The ML compiler knows about the structure of values according
+\<close>
+
+
+subsection \<open>Printing ML values\<close>
+
+text \<open>The ML compiler knows about the structure of values according
   to their static type, and can print them in the manner of its
   toplevel, although the details are non-portable.  The
   antiquotations @{ML_antiquotation_def "make_string"} and
   @{ML_antiquotation_def "print"} provide a quasi-portable way to
   refer to this potential capability of the underlying ML system in
   generic Isabelle/ML sources.
 
   This is occasionally useful for diagnostic or demonstration
   purposes.  Note that production-quality tools require proper
-  user-level error messages, avoiding raw ML values in the output. *}
-
-text %mlantiq {*
+  user-level error messages, avoiding raw ML values in the output.\<close>
+
+text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "make_string"} & : & @{text ML_antiquotation} \\
   @{ML_antiquotation_def "print"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 

   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}
-*}
-
-text %mlex {* The following artificial examples show how to produce
-  adhoc output of ML values for debugging purposes. *}
-
-ML {*
+\<close>
+
+text %mlex \<open>The following artificial examples show how to produce
+  adhoc output of ML values for debugging purposes.\<close>
+
+ML \<open>
   val x = 42;
   val y = true;
 
   writeln (@{make_string} {x = x, y = y});
 
   @{print} {x = x, y = y};
   @{print tracing} {x = x, y = y};
-*}
-
-
-section {* Canonical argument order \label{sec:canonical-argument-order} *}
-
-text {* Standard ML is a language in the tradition of @{text
+\<close>
+
+
+section \<open>Canonical argument order \label{sec:canonical-argument-order}\<close>
+
+text \<open>Standard ML is a language in the tradition of @{text
   "\<lambda>"}-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.

   insert a value @{text "a"}.  These can be composed naturally as
   @{text "insert c \<circ> insert b \<circ> insert a"}.  The slightly awkward
   inversion of the composition order is due to conventional
   mathematical notation, which can be easily amended as explained
   below.
-*}
-
-
-subsection {* Forward application and composition *}
-
-text {* Regular function application and infix notation works best for
+\<close>
+
+
+subsection \<open>Forward application and composition\<close>
+
+text \<open>Regular function application and infix notation works best for
   relatively deeply structured expressions, e.g.\ @{text "h (f x y + g
   z)"}.  The important special case of \emph{linear transformation}
   applies a cascade of functions @{text "f\<^sub>n (\<dots> (f\<^sub>1 x))"}.  This
   becomes hard to read and maintain if the functions are themselves
   given as complex expressions.  The notation can be significantly

   \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
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_op "|> ": "'a * ('a -> 'b) -> 'b"} \\
   @{index_ML_op "|-> ": "('c * 'a) * ('c -> 'a -> 'b) -> 'b"} \\
   @{index_ML_op "#> ": "('a -> 'b) * ('b -> 'c) -> 'a -> 'c"} \\
   @{index_ML_op "#-> ": "('a -> 'c * 'b) * ('c -> 'b -> 'd) -> 'a -> 'd"} \\
   \end{mldecls}
-*}
-
-
-subsection {* Canonical iteration *}
-
-text {* As explained above, a function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be
+\<close>
+
+
+subsection \<open>Canonical iteration\<close>
+
+text \<open>As explained above, a function @{text "f: \<alpha> \<rightarrow> \<beta> \<rightarrow> \<beta>"} can be
   understood as update on a configuration of type @{text "\<beta>"},
   parameterized by an argument of type @{text "\<alpha>"}.  Given @{text "a: \<alpha>"}
   the partial application @{text "(f a): \<beta> \<rightarrow> \<beta>"} operates
   homogeneously on @{text "\<beta>"}.  This can be iterated naturally over a
   list of parameters @{text "[a\<^sub>1, \<dots>, a\<^sub>n]"} as @{text "f a\<^sub>1 #> \<dots> #> f a\<^sub>n"}.

 
   The @{text "fold_map"} combinator essentially performs @{text
   "fold"} and @{text "map"} simultaneously: each application of @{text
   "f"} produces an updated configuration together with a side-result;
   the iteration collects all such side-results as a separate list.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{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}

   Isabelle library also has the historic @{ML Library.foldl} and @{ML
   Library.foldr}. To avoid unnecessary complication, all these historical
   versions should be ignored, and the canonical @{ML fold} (or @{ML fold_rev})
   used exclusively.
   \end{warn}
-*}
-
-text %mlex {* The following example shows how to fill a text buffer
+\<close>
+
+text %mlex \<open>The following example shows how to fill a text buffer
   incrementally by adding strings, either individually or from a given
   list.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   val s =
     Buffer.empty
     |> Buffer.add "digits: "
     |> fold (Buffer.add o string_of_int) (0 upto 9)
     |> Buffer.content;
 
   @{assert} (s = "digits: 0123456789");
-*}
-
-text {* Note how @{ML "fold (Buffer.add o string_of_int)"} above saves
+\<close>
+
+text \<open>Note how @{ML "fold (Buffer.add o string_of_int)"} above saves
   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
   iteration, demonstrating fast accumulation of tree content using a
   text buffer.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   datatype tree = Text of string | Elem of string * tree list;
 
   fun slow_content (Text txt) = txt
     | slow_content (Elem (name, ts)) =
         "<" ^ name ^ ">" ^

         fold add_content ts #>
         Buffer.add ("</" ^ name ^ ">");
 
   fun fast_content tree =
     Buffer.empty |> add_content tree |> Buffer.content;
-*}
-
-text {* The slowness of @{ML slow_content} is due to the @{ML implode} of
+\<close>
+
+text \<open>The slowness of @{ML slow_content} is due to the @{ML implode} of
   the recursive results, because it copies previously produced strings
   again and again.
 
   The incremental @{ML add_content} avoids this by operating on a
   buffer that is passed through in a linear fashion.  Using @{ML_text

 
   Note that @{ML fast_content} above is only defined as example.  In
   many practical situations, it is customary to provide the
   incremental @{ML add_content} only and leave the initialization and
   termination to the concrete application to the user.
-*}
-
-
-section {* Message output channels \label{sec:message-channels} *}
-
-text {* Isabelle provides output channels for different kinds of
+\<close>
+
+
+section \<open>Message output channels \label{sec:message-channels}\<close>
+
+text \<open>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

   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.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML writeln: "string -> unit"} \\
   @{index_ML tracing: "string -> unit"} \\
   @{index_ML warning: "string -> unit"} \\
   @{index_ML error: "string -> 'a"} % FIXME Output.error_message (!?) \\

   The message channels should be used in a message-oriented manner.
   This means that multi-line output that logically belongs together is
   issued by a single invocation of @{ML writeln} etc.\ with the
   functional concatenation of all message constituents.
   \end{warn}
-*}
-
-text %mlex {* The following example demonstrates a multi-line
+\<close>
+
+text %mlex \<open>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.
-*}
-
-ML_command {*
+\<close>
+
+ML_command \<open>
   warning (cat_lines
    ["Beware the Jabberwock, my son!",
     "The jaws that bite, the claws that catch!",
     "Beware the Jubjub Bird, and shun",
     "The frumious Bandersnatch!"]);
-*}
-
-
-section {* Exceptions \label{sec:exceptions} *}
-
-text {* The Standard ML semantics of strict functional evaluation
+\<close>
+
+
+section \<open>Exceptions \label{sec:exceptions}\<close>
+
+text \<open>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.
 

   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}
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML try: "('a -> 'b) -> 'a -> 'b option"} \\
   @{index_ML can: "('a -> 'b) -> 'a -> bool"} \\
   @{index_ML_exception ERROR: string} \\
   @{index_ML_exception Fail: string} \\

 
   Inserting @{ML Runtime.exn_trace} into ML code temporarily is
   useful for debugging, but not suitable for production code.
 
   \end{description}
-*}
-
-text %mlantiq {*
+\<close>
+
+text %mlantiq \<open>
   \begin{matharray}{rcl}
   @{ML_antiquotation_def "assert"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
   \begin{description}

   @{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}
-*}
-
-
-section {* Strings of symbols \label{sec:symbols} *}
-
-text {* A \emph{symbol} constitutes the smallest textual unit in
+\<close>
+
+
+section \<open>Strings of symbols \label{sec:symbols}\<close>
+
+text \<open>A \emph{symbol} constitutes the smallest textual unit in
   Isabelle/ML --- raw ML characters are normally not encountered at
   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:

   the standard {\LaTeX} setup of the Isabelle document preparation system
   would present ``\verb,\,\verb,<alpha>,'' as @{text "\<alpha>"}, and
   ``\verb,\,\verb,<^bold>,\verb,\,\verb,<alpha>,'' as @{text "\<^bold>\<alpha>"}. On-screen
   rendering usually works by mapping a finite subset of Isabelle symbols to
   suitable Unicode characters.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "Symbol.symbol": string} \\
   @{index_ML Symbol.explode: "string -> Symbol.symbol list"} \\
   @{index_ML Symbol.is_letter: "Symbol.symbol -> bool"} \\
   @{index_ML Symbol.is_digit: "Symbol.symbol -> bool"} \\

   somewhat anachronistic 8-bit or 16-bit characters, but the idea of
   exploding a string into a list of small strings was extended to
   ``symbols'' as explained above.  Thus Isabelle sources can refer to
   an infinite store of user-defined symbols, without having to worry
   about the multitude of Unicode encodings that have emerged over the
-  years.  *}
-
-
-section {* Basic data types *}
-
-text {* The basis library proposal of SML97 needs to be treated with
+  years.\<close>
+
+
+section \<open>Basic data types\<close>
+
+text \<open>The basis library proposal of SML97 needs 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 cause problems with
   the parallel evaluation model of Isabelle/ML (such as @{ML
   TextIO.print} or @{ML OS.Process.system}).
 
   Subsequently we give a brief overview of important operations on
   basic ML data types.
-*}
-
-
-subsection {* Characters *}
-
-text %mlref {*
+\<close>
+
+
+subsection \<open>Characters\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type char} \\
   \end{mldecls}
 
   \begin{description}

   \item 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}
-*}
-
-
-subsection {* Strings *}
-
-text %mlref {*
+\<close>
+
+
+subsection \<open>Strings\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type string} \\
   \end{mldecls}
 
   \begin{description}

   like ``\verb,\,\verb,<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}
-*}
-
-text %mlex {* The subsequent example illustrates the difference of
+\<close>
+
+text %mlex \<open>The subsequent example illustrates the difference of
   physical addressing of bytes versus logical addressing of symbols in
   Isabelle strings.
-*}
-
-ML_val {*
+\<close>
+
+ML_val \<open>
   val s = "\<A>";
 
   @{assert} (length (Symbol.explode s) = 1);
   @{assert} (size s = 4);
-*}
-
-text {* Note that in Unicode renderings of the symbol @{text "\<A>"},
+\<close>
+
+text \<open>Note that in Unicode renderings of the symbol @{text "\<A>"},
   variations of encodings like UTF-8 or UTF-16 pose delicate questions
   about the multi-byte representations of its codepoint, which is outside
   of the 16-bit address space of the original Unicode standard from
   the 1990-ies.  In Isabelle/ML it is just ``\verb,\,\verb,<A>,''
-  literally, using plain ASCII characters beyond any doubts. *}
-
-
-subsection {* Integers *}
-
-text %mlref {*
+  literally, using plain ASCII characters beyond any doubts.\<close>
+
+
+subsection \<open>Integers\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type int} \\
   \end{mldecls}
 
   \begin{description}

   @{ML_structure Int}.  Structure @{ML_structure Integer} in @{file
   "~~/src/Pure/General/integer.ML"} provides some additional
   operations.
 
   \end{description}
-*}
-
-
-subsection {* Time *}
-
-text %mlref {*
+\<close>
+
+
+subsection \<open>Time\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type Time.time} \\
   @{index_ML seconds: "real -> Time.time"} \\
   \end{mldecls}
 

   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}
-*}
-
-
-subsection {* Options *}
-
-text %mlref {*
+\<close>
+
+
+subsection \<open>Options\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML Option.map: "('a -> 'b) -> 'a option -> 'b option"} \\
   @{index_ML is_some: "'a option -> bool"} \\
   @{index_ML is_none: "'a option -> bool"} \\
   @{index_ML the: "'a option -> 'a"} \\
   @{index_ML these: "'a list option -> 'a list"} \\
   @{index_ML the_list: "'a option -> 'a list"} \\
   @{index_ML the_default: "'a -> 'a option -> 'a"} \\
   \end{mldecls}
-*}
-
-text {* Apart from @{ML Option.map} most other operations defined in
+\<close>
+
+text \<open>Apart from @{ML Option.map} most other operations defined in
   structure @{ML_structure Option} are alien to Isabelle/ML and never
   used.  The operations shown above are defined in @{file
-  "~~/src/Pure/General/basics.ML"}.  *}
-
-
-subsection {* Lists *}
-
-text {* Lists are ubiquitous in ML as simple and light-weight
+  "~~/src/Pure/General/basics.ML"}.\<close>
+
+
+subsection \<open>Lists\<close>
+
+text \<open>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. *}
-
-text %mlref {*
+  are predefined in the SML97 library.\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML cons: "'a -> 'a list -> 'a list"} \\
   @{index_ML member: "('b * 'a -> bool) -> 'a list -> 'b -> bool"} \\
   @{index_ML insert: "('a * 'a -> bool) -> 'a -> 'a list -> 'a list"} \\
   @{index_ML remove: "('b * 'a -> bool) -> 'b -> 'a list -> 'a list"} \\

   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}
-*}
-
-text %mlex {* Using canonical @{ML fold} together with @{ML cons} (or
+\<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
   extra applications of @{ML rev}.  The alternative @{ML fold_rev} can
   be used in the few situations, where alternation should be
   prevented.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   val items = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
 
   val list1 = fold cons items [];
   @{assert} (list1 = rev items);
 
   val list2 = fold_rev cons items [];
   @{assert} (list2 = items);
-*}
-
-text {* The subsequent example demonstrates how to \emph{merge} two
-  lists in a natural way. *}
-
-ML {*
+\<close>
+
+text \<open>The subsequent example demonstrates how to \emph{merge} two
+  lists in a natural way.\<close>
+
+ML \<open>
   fun merge_lists eq (xs, ys) = fold_rev (insert eq) ys xs;
-*}
-
-text {* Here the first list is treated conservatively: only the new
+\<close>
+
+text \<open>Here the first list is treated conservatively: only the new
   elements from the second list are inserted.  The inside-out order of
   insertion via @{ML 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 @{ML merge} as defined in
   @{file "~~/src/Pure/library.ML"}.
-*}
-
-
-subsection {* Association lists *}
-
-text {* The operations for association lists interpret a concrete list
+\<close>
+
+
+subsection \<open>Association lists\<close>
+
+text \<open>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.
-*}
-
-text {*
+\<close>
+
+text \<open>
   \begin{mldecls}
   @{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}

 
   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.
-*}
-
-
-subsection {* Unsynchronized references *}
-
-text %mlref {*
+\<close>
+
+
+subsection \<open>Unsynchronized references\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "'a Unsynchronized.ref"} \\
   @{index_ML Unsynchronized.ref: "'a -> 'a Unsynchronized.ref"} \\
   @{index_ML "!": "'a Unsynchronized.ref -> 'a"} \\
   @{index_ML_op ":=": "'a Unsynchronized.ref * 'a -> unit"} \\
   \end{mldecls}
-*}
-
-text {* Due to ubiquitous parallelism in Isabelle/ML (see also
+\<close>
+
+text \<open>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.
 

 
   \begin{warn}
   Never @{ML_text "open Unsynchronized"}, not even in a local scope!
   Pretending that mutable state is no problem is a very bad idea.
   \end{warn}
-*}
-
-
-section {* Thread-safe programming \label{sec:multi-threading} *}
-
-text {* Multi-threaded execution has become an everyday reality in
+\<close>
+
+
+section \<open>Thread-safe programming \label{sec:multi-threading}\<close>
+
+text \<open>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.
-*}
-
-
-subsection {* Multi-threading with shared memory *}
-
-text {* Multiple threads help to organize advanced operations of the
+\<close>
+
+
+subsection \<open>Multi-threading with shared memory\<close>
+
+text \<open>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

   \begin{warn}
   Parallel computing resources are managed centrally by the
   Isabelle/ML infrastructure.  User programs must not fork their own
   ML threads to perform heavy computations.
   \end{warn}
-*}
-
-
-subsection {* Critical shared resources *}
-
-text {* Thread-safeness is mainly concerned about concurrent
+\<close>
+
+
+subsection \<open>Critical shared resources\<close>
+
+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}
 

   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}
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML File.tmp_path: "Path.T -> Path.T"} \\
   @{index_ML serial_string: "unit -> string"} \\
   \end{mldecls}
 

 
   \item @{ML serial_string}~@{text "()"} creates a new serial number
   that is unique over the runtime of the Isabelle/ML process.
 
   \end{description}
-*}
-
-text %mlex {* The following example shows how to create unique
+\<close>
+
+text %mlex \<open>The following example shows how to create unique
   temporary file names.
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   val tmp1 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   val tmp2 = File.tmp_path (Path.basic ("foo" ^ serial_string ()));
   @{assert} (tmp1 <> tmp2);
-*}
-
-
-subsection {* Explicit synchronization *}
-
-text {* Isabelle/ML also provides some explicit synchronization
+\<close>
+
+
+subsection \<open>Explicit synchronization\<close>
+
+text \<open>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!

   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!
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
   @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
   \begin{mldecls}

   \end{description}
 
   There are some further variants of the @{ML
   Synchronized.guarded_access} combinator, see @{file
   "~~/src/Pure/Concurrent/synchronized.ML"} for details.
-*}
-
-text %mlex {* The following example implements a counter that produces
+\<close>
+
+text %mlex \<open>The following example implements a counter that produces
   positive integers that are unique over the runtime of the Isabelle
   process:
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   local
     val counter = Synchronized.var "counter" 0;
   in
     fun next () =
       Synchronized.guarded_access counter
         (fn i =>
           let val j = i + 1
           in SOME (j, j) end);
   end;
-*}
-
-ML {*
+\<close>
+
+ML \<open>
   val a = next ();
   val b = next ();
   @{assert} (a <> b);
-*}
-
-text {* \medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
+\<close>
+
+text \<open>\medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
   to implement a mailbox as synchronized variable over a purely
-  functional list. *}
-
-
-section {* Managed evaluation *}
-
-text {* Execution of Standard ML follows the model of strict
+  functional list.\<close>
+
+
+section \<open>Managed evaluation\<close>
+
+text \<open>Execution of Standard ML follows the model of strict
   functional evaluation with optional exceptions.  Evaluation happens
   whenever some function is applied to (sufficiently many)
   arguments. The result is either an explicit value or an implicit
   exception.
 

   evaluations that depend on other evaluations: exceptions stemming
   from shared sub-graphs are exposed exactly once and in the order of
   their original occurrence (e.g.\ when printed at the toplevel).
   Interrupt counts as neutral element here: it is treated as minimal
   information about some canceled evaluation process, and is absorbed
-  by the presence of regular program exceptions.  *}
-
-text %mlref {*
+  by the presence of regular program exceptions.\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "'a Exn.result"} \\
   @{index_ML Exn.capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{index_ML Exn.interruptible_capture: "('a -> 'b) -> 'a -> 'b Exn.result"} \\
   @{index_ML Exn.release: "'a Exn.result -> 'a"} \\

   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}
-*}
-
-
-subsection {* Parallel skeletons \label{sec:parlist} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Parallel skeletons \label{sec:parlist}\<close>
+
+text \<open>
   Algorithmic skeletons are combinators that operate on lists in
   parallel, in the manner of well-known @{text map}, @{text exists},
   @{text forall} etc.  Management of futures (\secref{sec:futures})
   and their results as reified exceptions is wrapped up into simple
   programming interfaces that resemble the sequential versions.

   corresponds to one evaluation task.  If the granularity is too
   coarse, the available CPUs are not saturated.  If it is too
   fine-grained, CPU cycles are wasted due to the overhead of
   organizing parallel processing.  In the worst case, parallel
   performance will be less than the sequential counterpart!
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \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}
 

   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}
-*}
-
-text %mlex {* Subsequently, the Ackermann function is evaluated in
-  parallel for some ranges of arguments. *}
-
-ML_val {*
+\<close>
+
+text %mlex \<open>Subsequently, the Ackermann function is evaluated in
+  parallel for some ranges of arguments.\<close>
+
+ML_val \<open>
   fun ackermann 0 n = n + 1
     | ackermann m 0 = ackermann (m - 1) 1
     | ackermann m n = ackermann (m - 1) (ackermann m (n - 1));
 
   Par_List.map (ackermann 2) (500 upto 1000);
   Par_List.map (ackermann 3) (5 upto 10);
-*}
-
-
-subsection {* Lazy evaluation *}
-
-text {*
+\<close>
+
+
+subsection \<open>Lazy evaluation\<close>
+
+text \<open>
   Classic lazy evaluation works via the @{text lazy}~/ @{text force} pair of
   operations: @{text lazy} to wrap an unevaluated expression, and @{text
   force} to evaluate it once and store its result persistently. Later
   invocations of @{text force} retrieve the stored result without another
   evaluation. Isabelle/ML refines this idea to accommodate the aspects of

   This means a lazy value is completely evaluated at most once, in a
   thread-safe manner. There might be multiple interrupted evaluation attempts,
   and multiple receivers of intermediate interrupt events. Interrupts are
   \emph{not} made persistent: later evaluation attempts start again from the
   original expression.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "'a lazy"} \\
   @{index_ML Lazy.lazy: "(unit -> 'a) -> 'a lazy"} \\
   @{index_ML Lazy.value: "'a -> 'a lazy"} \\
   @{index_ML Lazy.force: "'a lazy -> 'a"} \\

   \item @{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}
-*}
-
-
-subsection {* Futures \label{sec:futures} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Futures \label{sec:futures}\<close>
+
+text \<open>
   Futures help to organize parallel execution in a value-oriented manner, with
   @{text fork}~/ @{text join} as the main pair of operations, and some further
   variants; see also @{cite "Wenzel:2009" and "Wenzel:2013:ITP"}. Unlike lazy
   values, futures are evaluated strictly and spontaneously on separate worker
   threads. Futures may be canceled, which leads to interrupts on running

   Promises are managed in the same task queue, so regular futures may depend
   on them. This allows a form of reactive programming, where some promises are
   used as minimal elements (or guards) within the future dependency graph:
   when these promises are fulfilled the evaluation of subsequent futures
   starts spontaneously, according to their own inter-dependencies.
-*}
-
-text %mlref {*
+\<close>
+
+text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "'a future"} \\
   @{index_ML Future.fork: "(unit -> 'a) -> 'a future"} \\
   @{index_ML Future.forks: "Future.params -> (unit -> 'a) list -> 'a future list"} \\
   @{index_ML Future.join: "'a future -> 'a"} \\

   \item @{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