# HG changeset patch
# User wenzelm
# Date 1304438645 -7200
# Node ID 8f5d5d71add0fe4dcba9fade708348e698cb1e6c
# Parent  6b404fe4087761683db333ed1fba6c7dac9d7e31
some documentation of @{rail} antiquotation;

diff -r 6b404fe40877 -r 8f5d5d71add0 NEWS
--- a/NEWS	Tue May 03 17:31:16 2011 +0200
+++ b/NEWS	Tue May 03 18:04:05 2011 +0200
@@ -89,7 +89,8 @@
 *** Document preparation ***
 
 * Antiquotation @{rail} layouts railroad syntax diagrams; requires
-railsetup.sty included in the Isabelle distribution.
+railsetup.sty included in the Isabelle distribution; see also isar-ref
+manual.
 
 * Localized \isabellestyle switch can be used within blocks or groups
 like this:
diff -r 6b404fe40877 -r 8f5d5d71add0 doc-src/IsarRef/Thy/Document_Preparation.thy
--- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 17:31:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 18:04:05 2011 +0200
@@ -465,6 +465,115 @@
 *}
 
 
+section {* Railroad diagrams *}
+
+text {*
+  \begin{matharray}{rcl}
+    @{antiquotation_def "rail"} & : & @{text antiquotation} \\
+  \end{matharray}
+
+  @{rail "'rail' string"}
+
+  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 "
+  rule? + ';'
+  ;
+  rule: ((identifier | @{syntax antiquotation}) ':')? body
+  ;
+  body: concatenation + '|'
+  ;
+  concatenation: ((atom '?'?) +) (('*' | '+') atom?)?
+  ;
+  atom: '(' body? ')' | identifier |
+    '@'? (string | @{syntax antiquotation}) |
+    '\\\\\\\\'
+  "}
+
+  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.
+
+  Each @{text rule} defines a formal language (with optional name),
+  using a notation that is similar to EBNF or regular expressions with
+  recursion.  The meaning and visual appearance of these rail language
+  elements is illustrated by the following representative examples.
+
+  \begin{itemize}
+
+  \item Empty @{verbatim "()"}
+
+  @{rail "()"}
+
+  \item Nonterminal @{verbatim "A"}
+
+  @{rail "A"}
+
+  \item Nonterminal via Isabelle antiquotation
+  @{verbatim "@{syntax method}"}
+
+  @{rail "@{syntax method}"}
+
+  \item Terminal @{verbatim "'xyz'"}
+
+  @{rail "'xyz'"}
+
+  \item Terminal in keyword style @{verbatim "@'xyz'"}
+
+  @{rail "@'xyz'"}
+
+  \item Terminal via Isabelle antiquotation
+  @{verbatim "@@{method rule}"}
+
+  @{rail "@@{method rule}"}
+
+  \item Concatenation @{verbatim "A B C"}
+
+  @{rail "A B C"}
+
+  \item Linebreak @{verbatim "\\\\"} inside
+  concatenation\footnote{Strictly speaking, this is only a single
+  backslash, but the enclosing @{syntax string} syntax requires a
+  second one for escaping.} @{verbatim "A B C \\\\ D E F"}
+
+  @{rail "A B C \\ D E F"}
+
+  \item Variants @{verbatim "A | B | C"}
+
+  @{rail "A | B | C"}
+
+  \item Option @{verbatim "A ?"}
+
+  @{rail "A ?"}
+
+  \item Repetition @{verbatim "A *"}
+
+  @{rail "A *"}
+
+  \item Repetition with separator @{verbatim "A * sep"}
+
+  @{rail "A * sep"}
+
+  \item Strict repetition @{verbatim "A +"}
+
+  @{rail "A +"}
+
+  \item Strict repetition with separator @{verbatim "A + sep"}
+
+  @{rail "A + sep"}
+
+  \end{itemize}
+*}
+
+
 section {* Draft presentation *}
 
 text {*
diff -r 6b404fe40877 -r 8f5d5d71add0 doc-src/IsarRef/Thy/document/Document_Preparation.tex
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 17:31:16 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 18:04:05 2011 +0200
@@ -632,6 +632,289 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isamarkupsection{Railroad diagrams%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+    \indexdef{}{antiquotation}{rail}\hypertarget{antiquotation.rail}{\hyperlink{antiquotation.rail}{\mbox{\isa{rail}}}} & : & \isa{antiquotation} \\
+  \end{matharray}
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\isa{rail}}[]
+\rail@nont{\isa{string}}[]
+\rail@end
+\end{railoutput}
+
+
+  The \hyperlink{antiquotation.rail}{\mbox{\isa{rail}}} antiquotation allows to include syntax
+  diagrams into Isabelle documents.  {\LaTeX} requires the style file
+  \verb|~~/lib/texinputs/pdfsetup.sty|, which can be used via
+  \verb|\usepackage{pdfsetup}| in \verb|root.tex|, for
+  example.
+
+  The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
+
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@plus
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{rule}}[]
+\rail@endbar
+\rail@nextplus{2}
+\rail@cterm{\isa{{\isaliteral{3B}{\isacharsemicolon}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{3}{\isa{rule}}
+\rail@bar
+\rail@nextbar{1}
+\rail@bar
+\rail@nont{\isa{identifier}}[]
+\rail@nextbar{2}
+\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[]
+\rail@endbar
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@endbar
+\rail@nont{\isa{body}}[]
+\rail@end
+\rail@begin{2}{\isa{body}}
+\rail@plus
+\rail@nont{\isa{concatenation}}[]
+\rail@nextplus{1}
+\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{3}{\isa{concatenation}}
+\rail@plus
+\rail@nont{\isa{atom}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
+\rail@endbar
+\rail@nextplus{2}
+\rail@endplus
+\rail@bar
+\rail@nextbar{1}
+\rail@bar
+\rail@term{\isa{{\isaliteral{2A}{\isacharasterisk}}}}[]
+\rail@nextbar{2}
+\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nextbar{2}
+\rail@nont{\isa{atom}}[]
+\rail@endbar
+\rail@endbar
+\rail@end
+\rail@begin{6}{\isa{atom}}
+\rail@bar
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{body}}[]
+\rail@endbar
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@nextbar{2}
+\rail@nont{\isa{identifier}}[]
+\rail@nextbar{3}
+\rail@bar
+\rail@nextbar{4}
+\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[]
+\rail@endbar
+\rail@bar
+\rail@nont{\isa{string}}[]
+\rail@nextbar{4}
+\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[]
+\rail@endbar
+\rail@nextbar{5}
+\rail@term{\isa{{\isaliteral{5C}{\isacharbackslash}}{\isaliteral{5C}{\isacharbackslash}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+  The lexical syntax of \isa{{\isaliteral{22}{\isachardoublequote}}identifier{\isaliteral{22}{\isachardoublequote}}} coincides with that of
+  \hyperlink{syntax.ident}{\mbox{\isa{ident}}} in regular Isabelle syntax, but \isa{string} uses
+  single quotes instead of double quotes of the standard \hyperlink{syntax.string}{\mbox{\isa{string}}} category, to avoid extra escapes.
+
+  Each \isa{rule} defines a formal language (with optional name),
+  using a notation that is similar to EBNF or regular expressions with
+  recursion.  The meaning and visual appearance of these rail language
+  elements is illustrated by the following representative examples.
+
+  \begin{itemize}
+
+  \item Empty \verb|()|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@end
+\end{railoutput}
+
+
+  \item Nonterminal \verb|A|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@nont{\isa{A}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Nonterminal via Isabelle antiquotation
+  \verb|@{syntax method}|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Terminal \verb|'xyz'|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\isa{xyz}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Terminal in keyword style \verb|@'xyz'|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\isa{\isakeyword{xyz}}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Terminal via Isabelle antiquotation
+  \verb|@@{method rule}|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Concatenation \verb|A B C|
+
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@nont{\isa{A}}[]
+\rail@nont{\isa{B}}[]
+\rail@nont{\isa{C}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Linebreak \verb|\\| inside
+  concatenation\footnote{Strictly speaking, this is only a single
+  backslash, but the enclosing \hyperlink{syntax.string}{\mbox{\isa{string}}} syntax requires a
+  second one for escaping.} \verb|A B C \\ D E F|
+
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@nont{\isa{A}}[]
+\rail@nont{\isa{B}}[]
+\rail@nont{\isa{C}}[]
+\rail@cr{2}
+\rail@nont{\isa{D}}[]
+\rail@nont{\isa{E}}[]
+\rail@nont{\isa{F}}[]
+\rail@end
+\end{railoutput}
+
+
+  \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
+
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@bar
+\rail@nont{\isa{A}}[]
+\rail@nextbar{1}
+\rail@nont{\isa{B}}[]
+\rail@nextbar{2}
+\rail@nont{\isa{C}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+  \item Option \verb|A ?|
+
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{A}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+  \item Repetition \verb|A *|
+
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@plus
+\rail@nextplus{1}
+\rail@cnont{\isa{A}}[]
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+  \item Repetition with separator \verb|A * sep|
+
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@bar
+\rail@nextbar{1}
+\rail@plus
+\rail@nont{\isa{A}}[]
+\rail@nextplus{2}
+\rail@cnont{\isa{sep}}[]
+\rail@endplus
+\rail@endbar
+\rail@end
+\end{railoutput}
+
+
+  \item Strict repetition \verb|A +|
+
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@plus
+\rail@nont{\isa{A}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+  \item Strict repetition with separator \verb|A + sep|
+
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@plus
+\rail@nont{\isa{A}}[]
+\rail@nextplus{1}
+\rail@cnont{\isa{sep}}[]
+\rail@endplus
+\rail@end
+\end{railoutput}
+
+
+  \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsection{Draft presentation%
 }
 \isamarkuptrue%