src/Doc/Implementation/ML.thy

 
   The rest of the file is divided into sections, subsections,
   subsubsections, paragraphs etc.\ using a simple layout via ML
   comments as follows.
 
-\begin{verbatim}
-(*** section ***)
-
-(** subsection **)
-
-(* subsubsection *)
-
-(*short paragraph*)
-
-(*
-  long paragraph,
-  with more text
-*)
-\end{verbatim}
+  \begin{verbatim}
+  (*** section ***)
+
+  (** subsection **)
+
+  (* subsubsection *)
+
+  (*short paragraph*)
+
+  (*
+    long paragraph,
+    with more text
+  *)
+  \end{verbatim}
 
   As in regular typography, there is some extra space \emph{before}
   section headings that are adjacent to plain text, bit not other headings
   as in the example above.
 

 
   fun print_foo ctxt foo =
     let
       fun aux t = ... string_of_term ctxt t ...
     in ... end;
-
   \end{verbatim}
 
 
   \paragraph{Specific conventions.} Here are some specific name forms
   that occur frequently in the sources.

   forms:
 
   \begin{enumerate}
 
   \item a single ASCII character ``@{text "c"}'', for example
-  ``\verb,a,'',
+  ``@{verbatim a}'',
 
   \item a codepoint according to UTF-8 (non-ASCII byte sequence),
 
-  \item a regular symbol ``\verb,\,\verb,<,@{text "ident"}\verb,>,'',
-  for example ``\verb,\,\verb,<alpha>,'',
-
-  \item a control symbol ``\verb,\,\verb,<^,@{text "ident"}\verb,>,'',
-  for example ``\verb,\,\verb,<^bold>,'',
-
-  \item a raw symbol ``\verb,\,\verb,<^raw:,@{text text}\verb,>,''
-  where @{text text} consists of printable characters excluding
-  ``\verb,.,'' and ``\verb,>,'', for example
-  ``\verb,\,\verb,<^raw:$\sum_{i = 1}^n$>,'',
-
-  \item a numbered raw control symbol ``\verb,\,\verb,<^raw,@{text
-  n}\verb,>, where @{text n} consists of digits, for example
-  ``\verb,\,\verb,<^raw42>,''.
+  \item a regular symbol ``@{verbatim \<open>\\<close>}@{verbatim "<"}@{text
+  "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<alpha>"}'',
+
+  \item a control symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^"}@{text
+  "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'',
+
+  \item a raw symbol ``@{verbatim \<open>\\<close>}@{verbatim "<^raw:"}@{text
+  text}@{verbatim ">"}'' where @{text text} consists of printable characters
+  excluding ``@{verbatim "."}'' and ``@{verbatim ">"}'', for example
+  ``@{verbatim "\<^raw:$\sum_{i = 1}^n$>"}'',
+
+  \item a numbered raw control symbol ``@{verbatim \<open>\\<close>}@{verbatim
+  "<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for
+  example ``@{verbatim "\<^raw42>"}''.
 
   \end{enumerate}
 
   The @{text "ident"} syntax for symbol names is @{text "letter
   (letter | digit)\<^sup>*"}, where @{text "letter = A..Za..z"} and @{text
   "digit = 0..9"}.  There are infinitely many regular symbols and
   control symbols, but a fixed collection of standard symbols is
-  treated specifically.  For example, ``\verb,\,\verb,<alpha>,'' is
+  treated specifically.  For example, ``@{verbatim "\<alpha>"}'' is
   classified as a letter, which means it may occur within regular
   Isabelle identifiers.
 
   The character set underlying Isabelle symbols is 7-bit ASCII, but 8-bit
   character sequences are passed-through unchanged. Unicode/UCS data in UTF-8

   mathematical symbols, but within the core Isabelle/ML world there is no link
   to the standard collection of Isabelle regular symbols.
 
   \medskip Output of Isabelle symbols depends on the print mode. For example,
   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.
+  would present ``@{verbatim "\<alpha>"}'' as @{text "\<alpha>"}, and ``@{verbatim
+  "\<^bold>\<alpha>"}'' as @{text "\<^bold>\<alpha>"}. On-screen rendering usually works by mapping a
+  finite subset of Isabelle symbols to suitable Unicode characters.
 \<close>
 
 text %mlref \<open>
   \begin{mldecls}
   @{index_ML_type "Symbol.symbol": string} \\

   \item XML tree structure via YXML (see also @{cite "isabelle-sys"}),
   with @{ML YXML.parse_body} as key operation.
 
   \end{enumerate}
 
-  Note that Isabelle/ML string literals may refer Isabelle symbols
-  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.
+  Note that Isabelle/ML string literals may refer Isabelle symbols like
+  ``@{verbatim \<alpha>}'' natively, \emph{without} escaping the backslash. This is a
+  consequence of Isabelle treating all source text as strings of symbols,
+  instead of raw characters.
 
   \end{description}
 \<close>
 
 text %mlex \<open>The subsequent example illustrates the difference of

 
 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>,''
+  the 1990-ies.  In Isabelle/ML it is just ``@{verbatim \<A>}''
   literally, using plain ASCII characters beyond any doubts.\<close>
 
 
 subsection \<open>Integers\<close>
 

   the attempt to fulfill it causes an exception.
 
   \end{description}
 \<close>
 
-
 end