# HG changeset patch
# User wenzelm
# Date 1288084938 -7200
# Node ID 4c35be108990cd375a0a27b2b53d915766a36fff
# Parent  8728165d366e7278b034805c2b706a2fec350e71
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};

diff -r 8728165d366e -r 4c35be108990 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Tue Oct 26 11:06:12 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Tue Oct 26 11:22:18 2010 +0200
@@ -92,7 +92,7 @@
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
-  \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
+  \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
   low-level profiling of the underlying ML runtime system.  For
   Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
   profiling.
@@ -260,7 +260,7 @@
   @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
   @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
-  @{verbatim "datatype action = Update | Remove"} \\
+  @{ML_text "datatype action = Update | Remove"} \\
   @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
   \end{mldecls}
 
diff -r 8728165d366e -r 4c35be108990 doc-src/IsarImplementation/Thy/Isar.thy
--- a/doc-src/IsarImplementation/Thy/Isar.thy	Tue Oct 26 11:06:12 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Tue Oct 26 11:22:18 2010 +0200
@@ -361,7 +361,7 @@
   \medskip The following toy examples illustrate how the goal facts
   and state are passed to proof methods.  The pre-defined proof method
   called ``@{method tactic}'' wraps ML source of type @{ML_type
-  tactic} (abstracted over @{verbatim facts}).  This allows immediate
+  tactic} (abstracted over @{ML_text facts}).  This allows immediate
   experimentation without parsing of concrete syntax. *}
 
 example_proof
@@ -398,7 +398,7 @@
   The @{ML Attrib.thms} parser produces a list of theorems from the
   usual Isar syntax involving attribute expressions etc.\ (syntax
   category @{syntax thmrefs}) \cite{isabelle-isar-ref}.  The resulting
-  @{verbatim thms} are added to @{ML HOL_basic_ss} which already
+  @{ML_text thms} are added to @{ML HOL_basic_ss} which already
   contains the basic Simplifier setup for HOL.
 
   The tactic @{ML asm_full_simp_tac} is the one that is also used in
diff -r 8728165d366e -r 4c35be108990 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 26 11:06:12 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Tue Oct 26 11:22:18 2010 +0200
@@ -112,14 +112,14 @@
   \medskip
   \begin{tabular}{lll}
   variant & example & ML categories \\\hline
-  lower-case & @{verbatim foo_bar} & values, types, record fields \\
-  capitalized & @{verbatim Foo_Bar} & datatype constructors, structures, functors \\
-  upper-case & @{verbatim FOO_BAR} & special values, exception constructors, signatures \\
+  lower-case & @{ML_text foo_bar} & values, types, record fields \\
+  capitalized & @{ML_text Foo_Bar} & datatype constructors, structures, functors \\
+  upper-case & @{ML_text FOO_BAR} & special values, exception constructors, signatures \\
   \end{tabular}
   \medskip
 
   For historical reasons, many capitalized names omit underscores,
-  e.g.\ old-style @{verbatim FooBar} instead of @{verbatim Foo_Bar}.
+  e.g.\ old-style @{ML_text FooBar} instead of @{ML_text Foo_Bar}.
   Genuine mixed-case names are \emph{not} used, bacause clear division
   of words is essential for readability.\footnote{Camel-case was
   invented to workaround the lack of underscore in some early
@@ -128,12 +128,12 @@
 
   A single (capital) character does not count as ``word'' in this
   respect: some Isabelle/ML names are suffixed by extra markers like
-  this: @{verbatim foo_barT}.
+  this: @{ML_text foo_barT}.
 
-  Name variants are produced by adding 1--3 primes, e.g.\ @{verbatim
-  foo'}, @{verbatim foo''}, or @{verbatim foo'''}, but not @{verbatim
+  Name variants are produced by adding 1--3 primes, e.g.\ @{ML_text
+  foo'}, @{ML_text foo''}, or @{ML_text foo'''}, but not @{ML_text
   foo''''} or more.  Decimal digits scale better to larger numbers,
-  e.g.\ @{verbatim foo0}, @{verbatim foo1}, @{verbatim foo42}.
+  e.g.\ @{ML_text foo0}, @{ML_text foo1}, @{ML_text foo42}.
 
   \paragraph{Scopes.}  Apart from very basic library modules, ML
   structures are not ``opened'', but names are referenced with
@@ -147,7 +147,7 @@
   Local names of function abstraction or case/let bindings are
   typically shorter, sometimes using only rudiments of ``words'',
   while still avoiding cryptic shorthands.  An auxiliary function
-  called @{verbatim helper}, @{verbatim aux}, or @{verbatim f} is
+  called @{ML_text helper}, @{ML_text aux}, or @{ML_text f} is
   considered bad style.
 
   Example:
@@ -187,18 +187,18 @@
 
   \begin{itemize}
 
-  \item A function that maps @{verbatim foo} to @{verbatim bar} is
-  called @{verbatim foo_to_bar} or @{verbatim bar_of_foo} (never
-  @{verbatim foo2bar}, @{verbatim bar_from_foo}, @{verbatim
-  bar_for_foo}, or @{verbatim bar4foo}).
+  \item A function that maps @{ML_text foo} to @{ML_text bar} is
+  called @{ML_text foo_to_bar} or @{ML_text bar_of_foo} (never
+  @{ML_text foo2bar}, @{ML_text bar_from_foo}, @{ML_text
+  bar_for_foo}, or @{ML_text bar4foo}).
 
-  \item The name component @{verbatim legacy} means that the operation
+  \item The name component @{ML_text legacy} means that the operation
   is about to be discontinued soon.
 
-  \item The name component @{verbatim old} means that this is historic
+  \item The name component @{ML_text old} means that this is historic
   material that might disappear at some later stage.
 
-  \item The name component @{verbatim global} means that this works
+  \item The name component @{ML_text global} means that this works
   with the background theory instead of the regular local context
   (\secref{sec:context}), sometimes for historical reasons, sometimes
   due a genuine lack of locality of the concept involved, sometimes as
@@ -213,23 +213,23 @@
 
   \begin{itemize}
 
-  \item theories are called @{verbatim thy}, rarely @{verbatim theory}
-  (never @{verbatim thry})
+  \item theories are called @{ML_text thy}, rarely @{ML_text theory}
+  (never @{ML_text thry})
 
-  \item proof contexts are called @{verbatim ctxt}, rarely @{verbatim
-  context} (never @{verbatim ctx})
+  \item proof contexts are called @{ML_text ctxt}, rarely @{ML_text
+  context} (never @{ML_text ctx})
 
-  \item generic contexts are called @{verbatim context}, rarely
-  @{verbatim ctxt}
+  \item generic contexts are called @{ML_text context}, rarely
+  @{ML_text ctxt}
 
-  \item local theories are called @{verbatim lthy}, except for local
+  \item local theories are called @{ML_text lthy}, except for local
   theories that are treated as proof context (which is a semantic
   super-type)
 
   \end{itemize}
 
   Variations with primed or decimal numbers are always possible, as
-  well as sematic prefixes like @{verbatim foo_thy} or @{verbatim
+  well as sematic prefixes like @{ML_text foo_thy} or @{ML_text
   bar_ctxt}, but the base conventions above need to be preserved.
   This allows to visualize the their data flow via plain regular
   expressions in the editor.
@@ -239,28 +239,28 @@
 
   \begin{itemize}
 
-  \item sorts are called @{verbatim S}
+  \item sorts are called @{ML_text S}
 
-  \item types are called @{verbatim T}, @{verbatim U}, or @{verbatim
-  ty} (never @{verbatim t})
+  \item types are called @{ML_text T}, @{ML_text U}, or @{ML_text
+  ty} (never @{ML_text t})
 
-  \item terms are called @{verbatim t}, @{verbatim u}, or @{verbatim
-  tm} (never @{verbatim trm})
+  \item terms are called @{ML_text t}, @{ML_text u}, or @{ML_text
+  tm} (never @{ML_text trm})
 
-  \item certified types are called @{verbatim cT}, rarely @{verbatim
+  \item certified types are called @{ML_text cT}, rarely @{ML_text
   T}, with variants as for types
 
-  \item certified terms are called @{verbatim ct}, rarely @{verbatim
+  \item certified terms are called @{ML_text ct}, rarely @{ML_text
   t}, with variants as for terms
 
-  \item theorems are called @{verbatim th}, or @{verbatim thm}
+  \item theorems are called @{ML_text th}, or @{ML_text thm}
 
   \end{itemize}
 
   Proper semantic names override these conventions completely.  For
   example, the left-hand side of an equation (as a term) can be called
-  @{verbatim lhs} (not @{verbatim lhs_tm}).  Or a term that is known
-  to be a variable can be called @{verbatim v} or @{verbatim x}.
+  @{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}.
 
   \end{itemize}
 *}
@@ -309,17 +309,17 @@
     c);
   \end{verbatim}
 
-  Some special infixes (e.g.\ @{verbatim "|>"}) work better at the
+  Some special infixes (e.g.\ @{ML_text "|>"}) work better at the
   start of the line, but punctuation is always at the end.
 
   Function application follows the tradition of @{text "\<lambda>"}-calculus,
-  not informal mathematics.  For example: @{verbatim "f a b"} for a
-  curried function, or @{verbatim "g (a, b)"} for a tupled function.
-  Note that the space between @{verbatim g} and the pair @{verbatim
+  not informal mathematics.  For example: @{ML_text "f a b"} for a
+  curried function, or @{ML_text "g (a, b)"} for a tupled function.
+  Note that the space between @{ML_text g} and the pair @{ML_text
   "(a, b)"} follows the important principle of
-  \emph{compositionality}: the layout of @{verbatim "g p"} does not
-  change when @{verbatim "p"} is refined to the concrete pair
-  @{verbatim "(a, b)"}.
+  \emph{compositionality}: the layout of @{ML_text "g p"} does not
+  change when @{ML_text "p"} is refined to the concrete pair
+  @{ML_text "(a, b)"}.
 
   \paragraph{Indentation} uses plain spaces, never hard
   tabulators.\footnote{Tabulators were invented to move the carriage
@@ -366,13 +366,13 @@
   avoided.
 
   \paragraph{Complex expressions} that consist of multi-clausal
-  function definitions, @{verbatim handle}, @{verbatim case},
-  @{verbatim let} (and combinations) require special attention.  The
+  function definitions, @{ML_text handle}, @{ML_text case},
+  @{ML_text let} (and combinations) require special attention.  The
   syntax of Standard ML is quite ambitious and admits a lot of
   variance that can distort the meaning of the text.
 
-  Clauses of @{verbatim fun}, @{verbatim fn}, @{verbatim handle},
-  @{verbatim case} get extra indentation to indicate the nesting
+  Clauses of @{ML_text fun}, @{ML_text fn}, @{ML_text handle},
+  @{ML_text case} get extra indentation to indicate the nesting
   clearly.  Example:
 
   \begin{verbatim}
@@ -392,7 +392,7 @@
     expr2
   \end{verbatim}
 
-  Body expressions consisting of @{verbatim case} or @{verbatim let}
+  Body expressions consisting of @{ML_text case} or @{ML_text let}
   require care to maintain compositionality, to prevent loss of
   logical indentation where it is especially important to see the
   structure of the text.  Example:
@@ -425,7 +425,7 @@
     end
   \end{verbatim}
 
-  Extra parentheses around @{verbatim case} expressions are optional,
+  Extra parentheses around @{ML_text case} expressions are optional,
   but help to analyse the nesting based on character matching in the
   editor.
 
@@ -434,7 +434,7 @@
 
   \begin{enumerate}
 
-  \item @{verbatim "if"} expressions are iterated as if there would be
+  \item @{ML_text "if"} expressions are iterated as if there would be
   a multi-branch conditional in SML, e.g.
 
   \begin{verbatim}
@@ -445,7 +445,7 @@
   else e3
   \end{verbatim}
 
-  \item @{verbatim fn} abstractions are often layed-out as if they
+  \item @{ML_text fn} abstractions are often layed-out as if they
   would lack any structure by themselves.  This traditional form is
   motivated by the possibility to shift function arguments back and
   forth wrt.\ additional combinators.  Example:
@@ -457,13 +457,13 @@
     expr)
   \end{verbatim}
 
-  Here the visual appearance is that of three arguments @{verbatim x},
-  @{verbatim y}, @{verbatim z}.
+  Here the visual appearance is that of three arguments @{ML_text x},
+  @{ML_text y}, @{ML_text z}.
 
   \end{enumerate}
 
   Such weakly structured layout should be use with great care.  Here
-  is a counter-example involving @{verbatim let} expressions:
+  is a counter-example involving @{ML_text let} expressions:
 
   \begin{verbatim}
   (* WRONG *)
@@ -945,7 +945,7 @@
   again.
 
   The incremental @{ML add_content} avoids this by operating on a
-  buffer that is passed through in a linear fashion.  Using @{verbatim
+  buffer that is passed through in a linear fashion.  Using @{ML_text
   "#>"} and contraction over the actual buffer argument saves some
   additional boiler-plate.  Of course, the two @{ML "Buffer.add"}
   invocations with concatenated strings could have been split into
@@ -1106,7 +1106,7 @@
   Traditionally, the (short) exception message would include the name
   of an ML function, although this is no longer necessary, because the
   ML runtime system prints a detailed source position of the
-  corresponding @{verbatim raise} keyword.
+  corresponding @{ML_text raise} keyword.
 
   \medskip User modules can always introduce their own custom
   exceptions locally, e.g.\ to organize internal failures robustly
@@ -1163,8 +1163,8 @@
   \item @{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 @{verbatim "(SOME"}~@{text "f
-  x"}~@{verbatim "handle _ => NONE)"} that is occasionally seen in
+  for the \emph{unsafe} version @{ML_text "(SOME"}~@{text "f
+  x"}~@{ML_text "handle _ => NONE)"} that is occasionally seen in
   books about SML.
 
   \item @{ML can} is similar to @{ML try} with more abstract result.
@@ -1183,8 +1183,8 @@
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML exception_trace}~@{verbatim "(fn () =>"}~@{text
-  "e"}@{verbatim ")"} evaluates expression @{text "e"} while printing
+  \item @{ML exception_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).\footnote{In versions of Poly/ML the
   trace will appear on raw stdout of the Isabelle process.}