src/Doc/IsarRef/Document_Preparation.thy

 
   Note that formal comments (\secref{sec:comments}) are similar to
   markup commands, but have a different status within Isabelle/Isar
   syntax.
 
-  @{rail "
+  @{rail \<open>
     (@@{command chapter} | @@{command section} | @@{command subsection} |
       @@{command subsubsection} | @@{command text}) @{syntax target}? @{syntax text}
     ;
     (@@{command header} | @@{command text_raw} | @@{command sect} | @@{command subsect} |
       @@{command subsubsect} | @@{command txt} | @@{command txt_raw}) @{syntax text}
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{command header} provides plain text markup just preceding
   the formal beginning of a theory.  The corresponding {\LaTeX} macro

   informal explanation is achieved, since terms and types appearing in
   antiquotations are checked within the current theory or proof
   context.
 
   %% FIXME less monolithic presentation, move to individual sections!?
-  @{rail "
+  @{rail \<open>
     '@{' antiquotation '}'
     ;
     @{syntax_def antiquotation}:
       @@{antiquotation theory} options @{syntax name} |
       @@{antiquotation thm} options styles @{syntax thmrefs} |

       @@{antiquotation full_prf} options @{syntax thmrefs} |
       @@{antiquotation ML} options @{syntax name} |
       @@{antiquotation ML_op} options @{syntax name} |
       @@{antiquotation ML_type} options @{syntax name} |
       @@{antiquotation ML_struct} options @{syntax name} |
-      @@{antiquotation \"file\"} options @{syntax name} |
+      @@{antiquotation "file"} options @{syntax name} |
       @@{antiquotation file_unchecked} options @{syntax name} |
       @@{antiquotation url} options @{syntax name}
     ;
     options: '[' (option * ',') ']'
     ;
     option: @{syntax name} | @{syntax name} '=' @{syntax name}
     ;
     styles: '(' (style + ',') ')'
     ;
     style: (@{syntax name} +)
-  "}
+  \<close>}
 
   Note that the syntax of antiquotations may \emph{not} include source
   comments @{verbatim "(*"}~@{text "\<dots>"}~@{verbatim "*)"} nor verbatim
   text @{verbatim "{"}@{verbatim "*"}~@{text "\<dots>"}~@{verbatim
   "*"}@{verbatim "}"}.

 
 text {* Each Isabelle/Isar command may be decorated by additional
   presentation tags, to indicate some modification in the way it is
   printed in the document.
 
-  @{rail "
+  @{rail \<open>
     @{syntax_def tags}: ( tag * )
     ;
     tag: '%' (@{syntax ident} | @{syntax string})
-  "}
+  \<close>}
 
   Some tags are pre-declared for certain classes of commands, serving
   as default markup if no tags are given in the text:
 
   \medskip

 text {*
   \begin{matharray}{rcl}
     @{antiquotation_def "rail"} & : & @{text antiquotation} \\
   \end{matharray}
 
-  @{rail "'rail' string"}
+  @{rail \<open>'rail' (string | cartouche)\<close>}
 
   The @{antiquotation rail} antiquotation allows to include syntax
   diagrams into Isabelle documents.  {\LaTeX} requires the style file
   @{file "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
   @{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for
   example.
 
   The rail specification language is quoted here as Isabelle @{syntax
   string}; it has its own grammar given below.
 
-  @{rail "
+  @{rail \<open>
   rule? + ';'
   ;
   rule: ((identifier | @{syntax antiquotation}) ':')? body
   ;
   body: concatenation + '|'
   ;
   concatenation: ((atom '?'?) +) (('*' | '+') atom?)?
   ;
   atom: '(' body? ')' | identifier |
     '@'? (string | @{syntax antiquotation}) |
-    '\\\\\\\\'
-  "}
+    '\<newline>'
+  \<close>}
 
   The lexical syntax of @{text "identifier"} coincides with that of
   @{syntax ident} in regular Isabelle syntax, but @{text string} uses
   single quotes instead of double quotes of the standard @{syntax
   string} category, to avoid extra escapes.

 
   \begin{itemize}
 
   \item Empty @{verbatim "()"}
 
-  @{rail "()"}
+  @{rail \<open>()\<close>}
 
   \item Nonterminal @{verbatim "A"}
 
-  @{rail "A"}
+  @{rail \<open>A\<close>}
 
   \item Nonterminal via Isabelle antiquotation
   @{verbatim "@{syntax method}"}
 
-  @{rail "@{syntax method}"}
+  @{rail \<open>@{syntax method}\<close>}
 
   \item Terminal @{verbatim "'xyz'"}
 
-  @{rail "'xyz'"}
+  @{rail \<open>'xyz'\<close>}
 
   \item Terminal in keyword style @{verbatim "@'xyz'"}
 
-  @{rail "@'xyz'"}
+  @{rail \<open>@'xyz'\<close>}
 
   \item Terminal via Isabelle antiquotation
   @{verbatim "@@{method rule}"}
 
-  @{rail "@@{method rule}"}
+  @{rail \<open>@@{method rule}\<close>}
 
   \item Concatenation @{verbatim "A B C"}
 
-  @{rail "A B C"}
+  @{rail \<open>A B C\<close>}
 
   \item Newline inside concatenation
   @{verbatim "A B C \<newline> D E F"}
 
-  @{rail "A B C \<newline> D E F"}
+  @{rail \<open>A B C \<newline> D E F\<close>}
 
   \item Variants @{verbatim "A | B | C"}
 
-  @{rail "A | B | C"}
+  @{rail \<open>A | B | C\<close>}
 
   \item Option @{verbatim "A ?"}
 
-  @{rail "A ?"}
+  @{rail \<open>A ?\<close>}
 
   \item Repetition @{verbatim "A *"}
 
-  @{rail "A *"}
+  @{rail \<open>A *\<close>}
 
   \item Repetition with separator @{verbatim "A * sep"}
 
-  @{rail "A * sep"}
+  @{rail \<open>A * sep\<close>}
 
   \item Strict repetition @{verbatim "A +"}
 
-  @{rail "A +"}
+  @{rail \<open>A +\<close>}
 
   \item Strict repetition with separator @{verbatim "A + sep"}
 
-  @{rail "A + sep"}
+  @{rail \<open>A + sep\<close>}
 
   \end{itemize}
 *}
 
 

 text {*
   \begin{matharray}{rcl}
     @{command_def "display_drafts"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     @@{command display_drafts} (@{syntax name} +)
-
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{command "display_drafts"}~@{text paths} performs simple output of a
   given list of raw source files. Only those symbols that do not require