# HG changeset patch # User wenzelm # Date 1413830582 -7200 # Node ID 33be43d701474b386ba82140c0674a9799148da6 # Parent 9cd739562c71811e61d0dec819f9ad6d4f44f186 more antiquotations; tuned spacing; diff -r 9cd739562c71 -r 33be43d70147 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Mon Oct 20 17:56:23 2014 +0200 +++ b/src/Doc/Implementation/ML.thy Mon Oct 20 20:43:02 2014 +0200 @@ -76,20 +76,20 @@ 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 @@ -180,7 +180,6 @@ let fun aux t = ... string_of_term ctxt t ... in ... end; - \end{verbatim} @@ -1252,24 +1251,24 @@ \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,,'', - - \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 \\\}@{verbatim "<"}@{text + "ident"}@{verbatim ">"}'', for example ``@{verbatim "\"}'', + + \item a control symbol ``@{verbatim \\\}@{verbatim "<^"}@{text + "ident"}@{verbatim ">"}'', for example ``@{verbatim "\<^bold>"}'', + + \item a raw symbol ``@{verbatim \\\}@{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 \\\}@{verbatim + "<^raw"}@{text n}@{verbatim ">"}, where @{text n} consists of digits, for + example ``@{verbatim "\<^raw42>"}''. \end{enumerate} @@ -1277,7 +1276,7 @@ (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,,'' is + treated specifically. For example, ``@{verbatim "\"}'' is classified as a letter, which means it may occur within regular Isabelle identifiers. @@ -1290,10 +1289,9 @@ \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,,'' as @{text "\"}, and - ``\verb,\,\verb,<^bold>,\verb,\,\verb,,'' as @{text "\<^bold>\"}. On-screen - rendering usually works by mapping a finite subset of Isabelle symbols to - suitable Unicode characters. + would present ``@{verbatim "\"}'' as @{text "\"}, and ``@{verbatim + "\<^bold>\"}'' as @{text "\<^bold>\"}. On-screen rendering usually works by mapping a + finite subset of Isabelle symbols to suitable Unicode characters. \ text %mlref \ @@ -1409,10 +1407,10 @@ \end{enumerate} - Note that Isabelle/ML string literals may refer Isabelle symbols - like ``\verb,\,\verb,,'' 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 \}'' 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} \ @@ -1433,7 +1431,7 @@ 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,,'' + the 1990-ies. In Isabelle/ML it is just ``@{verbatim \}'' literally, using plain ASCII characters beyond any doubts.\ @@ -2339,5 +2337,4 @@ \end{description} \ - end diff -r 9cd739562c71 -r 33be43d70147 src/Doc/Implementation/Prelim.thy --- a/src/Doc/Implementation/Prelim.thy Mon Oct 20 17:56:23 2014 +0200 +++ b/src/Doc/Implementation/Prelim.thy Mon Oct 20 20:43:02 2014 +0200 @@ -611,7 +611,7 @@ ``@{text "Foo.bar.baz"}'' is considered as a long name consisting of qualifier @{text "Foo.bar"} and base name @{text "baz"}. The individual constituents of a name may have further substructure, - e.g.\ the string ``\verb,\,\verb,,'' encodes as a single + e.g.\ the string ``@{verbatim \}'' encodes as a single symbol (\secref{sec:symbols}). \medskip Subsequently, we shall introduce specific categories of diff -r 9cd739562c71 -r 33be43d70147 src/Doc/System/Basics.thy --- a/src/Doc/System/Basics.thy Mon Oct 20 17:56:23 2014 +0200 +++ b/src/Doc/System/Basics.thy Mon Oct 20 20:43:02 2014 +0200 @@ -322,8 +322,8 @@ that directory exists). This allows to install private components via @{file_unchecked "$ISABELLE_HOME_USER/etc/components"}, although it is often more convenient to do that programmatically via the - \verb,init_component, shell function in the \verb,etc/settings, - script of \verb,$ISABELLE_HOME_USER, (or any other component + @{verbatim init_component} shell function in the @{verbatim "etc/settings"} + script of @{verbatim "$ISABELLE_HOME_USER"} (or any other component directory). For example: \begin{ttbox} init_component "$HOME/screwdriver-2.0"