
diff -r 4f169d2cf6f3 -r 782f0b662cae src/Doc/Implementation/ML.thy
--- a/src/Doc/Implementation/ML.thy	Tue Oct 07 21:28:24 2014 +0200
+++ b/src/Doc/Implementation/ML.thy	Tue Oct 07 21:29:59 2014 +0200
@@ -4,9 +4,9 @@
 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
@@ -27,12 +27,12 @@
   @{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
@@ -57,12 +57,12 @@
   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.
@@ -98,12 +98,12 @@
   \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
@@ -282,12 +282,12 @@
   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.
@@ -519,12 +519,12 @@
   \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
@@ -544,12 +544,12 @@
   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
@@ -559,20 +559,20 @@
   @{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.
@@ -589,18 +589,18 @@
   @{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.
@@ -612,29 +612,29 @@
   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"} \\
@@ -667,12 +667,12 @@
   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:
 
@@ -691,12 +691,12 @@
   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
@@ -706,9 +706,9 @@
 
   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} \\
@@ -733,12 +733,12 @@
   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;
 
@@ -746,12 +746,12 @@
 
   @{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
@@ -818,12 +818,12 @@
   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
@@ -853,21 +853,21 @@
   @{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
@@ -891,9 +891,9 @@
   "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"} \\
@@ -923,14 +923,14 @@
   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: "
@@ -938,9 +938,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
@@ -949,9 +949,9 @@
   \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
@@ -968,9 +968,9 @@
 
   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.
 
@@ -994,12 +994,12 @@
   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.
 
@@ -1015,9 +1015,9 @@
   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"} \\
@@ -1082,25 +1082,25 @@
   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
@@ -1175,9 +1175,9 @@
   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"} \\
@@ -1222,9 +1222,9 @@
   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}
@@ -1237,12 +1237,12 @@
   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
@@ -1294,9 +1294,9 @@
   ``\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"} \\
@@ -1348,12 +1348,12 @@
   ``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
@@ -1362,12 +1362,12 @@
 
   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}
@@ -1379,12 +1379,12 @@
   \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}
@@ -1415,31 +1415,31 @@
   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}
@@ -1461,12 +1461,12 @@
   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"} \\
@@ -1485,12 +1485,12 @@
   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"} \\
@@ -1500,22 +1500,22 @@
   @{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"} \\
@@ -1546,17 +1546,17 @@
   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 [];
@@ -1564,16 +1564,16 @@
 
   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.
@@ -1581,19 +1581,19 @@
   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"} \\
@@ -1623,21 +1623,21 @@
   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
@@ -1654,12 +1654,12 @@
   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
@@ -1670,12 +1670,12 @@
 
   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
@@ -1725,12 +1725,12 @@
   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.
 
@@ -1798,9 +1798,9 @@
   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"} \\
@@ -1816,22 +1816,22 @@
   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
@@ -1856,9 +1856,9 @@
   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"} \\
@@ -1907,14 +1907,14 @@
   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
@@ -1924,22 +1924,22 @@
           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
@@ -1983,9 +1983,9 @@
   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"} \\
@@ -2029,12 +2029,12 @@
   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})
@@ -2048,9 +2048,9 @@
   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"} \\
@@ -2081,24 +2081,24 @@
   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
@@ -2119,9 +2119,9 @@
   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"} \\
@@ -2148,12 +2148,12 @@
   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
@@ -2203,9 +2203,9 @@
   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"} \\
@@ -2337,7 +2337,7 @@
   the attempt to fulfill it causes an exception.
 
   \end{description}
-*}
+\<close>
 
 
 end




