# HG changeset patch
# User wenzelm
# Date 1226609809 -3600
# Node ID 4510201c6aaf5c6629ccdde1af1eef3a83573669
# Parent  93a372e2dc7aaebf8e9c9df2173b99a404bdbc89
mixfix annotations: verbatim for special symbols;

diff -r 93a372e2dc7a -r 4510201c6aaf doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:56:23 2008 +0100
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Nov 13 21:56:49 2008 +0100
@@ -304,49 +304,57 @@
 
   \begin{itemize}
 
-  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
-  sequence of characters other than the special characters @{text "'"}
-  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
-  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
-  (parentheses).
+  \item @{text "d"} is a delimiter, namely a non-empty sequence of
+  characters other than the following special characters:
 
-  A single quote escapes the special meaning of these meta-characters,
-  producing a literal version of the following character, unless that
-  is a blank.  A single quote followed by a blank separates
-  delimiters, without affecting printing, but input tokens may have
-  additional white space here.
+  \smallskip
+  \begin{tabular}{ll}
+    @{verbatim "'"} & single quote \\
+    @{verbatim "_"} & underscore \\
+    @{text "\<index>"} & index symbol \\
+    @{verbatim "("} & open parenthesis \\
+    @{verbatim ")"} & close parenthesis \\
+    @{verbatim "/"} & slash \\
+  \end{tabular}
+  \medskip
 
-  \item @{text "_"} is an argument position, which stands for a
+  \item @{verbatim "'"} escapes the special meaning of these
+  meta-characters, producing a literal version of the following
+  character, unless that is a blank.
+
+  A single quote followed by a blank separates delimiters, without
+  affecting printing, but input tokens may have additional white space
+  here.
+
+  \item @{verbatim "_"} is an argument position, which stands for a
   certain syntactic category in the underlying grammar.
 
-  \item @{text "\<index>"} is an indexed argument position; this is
-  the place where implicit structure arguments can be attached.
+  \item @{text "\<index>"} is an indexed argument position; this is the place
+  where implicit structure arguments can be attached.
 
-  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
-  printing.  This and the following specifications do not affect
-  parsing at all.
+  \item @{text "s"} is a non-empty sequence of spaces for printing.
+  This and the following specifications do not affect parsing at all.
 
-  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
+  \item @{verbatim "("}@{text n} opens a pretty printing block.  The
   optional number specifies how much indentation to add when a line
   break occurs within the block.  If the parenthesis is not followed
   by digits, the indentation defaults to 0.  A block specified via
-  @{text "(00"} is unbreakable.
+  @{verbatim "(00"} is unbreakable.
 
-  \item @{text ")"} closes a pretty printing block.
+  \item @{verbatim ")"} closes a pretty printing block.
 
-  \item @{text "//"} forces a line break.
+  \item @{verbatim "//"} forces a line break.
 
-  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
-  "\<^bold>s"} stands for the string of spaces (zero or more) right
-  after the slash.  These spaces are printed if the break is
-  \emph{not} taken.
+  \item @{verbatim "/"}@{text s} allows a line break.  Here @{text s}
+  stands for the string of spaces (zero or more) right after the
+  slash.  These spaces are printed if the break is \emph{not} taken.
 
   \end{itemize}
 
-  For example, the template @{text "(_ +/ _)"} specifies an infix
-  operator.  There are two argument positions; the delimiter @{text
-  "+"} is preceded by a space and followed by a space or line break;
-  the entire phrase is a pretty printing block.
+  For example, the template @{verbatim "(_ +/ _)"} specifies an infix
+  operator.  There are two argument positions; the delimiter
+  @{verbatim "+"} is preceded by a space and followed by a space or
+  line break; the entire phrase is a pretty printing block.
 
   The general idea of pretty printing with blocks and breaks is also
   described in \cite{paulson-ml2}.