1.1 --- a/NEWS	Tue May 03 17:31:16 2011 +0200
     1.2 +++ b/NEWS	Tue May 03 18:04:05 2011 +0200
     1.3 @@ -89,7 +89,8 @@
     1.4  *** Document preparation ***
     1.5  
     1.6  * Antiquotation @{rail} layouts railroad syntax diagrams; requires
     1.7 -railsetup.sty included in the Isabelle distribution.
     1.8 +railsetup.sty included in the Isabelle distribution; see also isar-ref
     1.9 +manual.
    1.10  
    1.11  * Localized \isabellestyle switch can be used within blocks or groups
    1.12  like this:

     2.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 17:31:16 2011 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Tue May 03 18:04:05 2011 +0200
     2.3 @@ -465,6 +465,115 @@
     2.4  *}
     2.5  
     2.6  
     2.7 +section {* Railroad diagrams *}
     2.8 +
     2.9 +text {*
    2.10 +  \begin{matharray}{rcl}
    2.11 +    @{antiquotation_def "rail"} & : & @{text antiquotation} \\
    2.12 +  \end{matharray}
    2.13 +
    2.14 +  @{rail "'rail' string"}
    2.15 +
    2.16 +  The @{antiquotation rail} antiquotation allows to include syntax
    2.17 +  diagrams into Isabelle documents.  {\LaTeX} requires the style file
    2.18 +  @{"file" "~~/lib/texinputs/pdfsetup.sty"}, which can be used via
    2.19 +  @{verbatim "\\usepackage{pdfsetup}"} in @{verbatim "root.tex"}, for
    2.20 +  example.
    2.21 +
    2.22 +  The rail specification language is quoted here as Isabelle @{syntax
    2.23 +  string}; it has its own grammar given below.
    2.24 +
    2.25 +  @{rail "
    2.26 +  rule? + ';'
    2.27 +  ;
    2.28 +  rule: ((identifier | @{syntax antiquotation}) ':')? body
    2.29 +  ;
    2.30 +  body: concatenation + '|'
    2.31 +  ;
    2.32 +  concatenation: ((atom '?'?) +) (('*' | '+') atom?)?
    2.33 +  ;
    2.34 +  atom: '(' body? ')' | identifier |
    2.35 +    '@'? (string | @{syntax antiquotation}) |
    2.36 +    '\\\\\\\\'
    2.37 +  "}
    2.38 +
    2.39 +  The lexical syntax of @{text "identifier"} coincides with that of
    2.40 +  @{syntax ident} in regular Isabelle syntax, but @{text string} uses
    2.41 +  single quotes instead of double quotes of the standard @{syntax
    2.42 +  string} category, to avoid extra escapes.
    2.43 +
    2.44 +  Each @{text rule} defines a formal language (with optional name),
    2.45 +  using a notation that is similar to EBNF or regular expressions with
    2.46 +  recursion.  The meaning and visual appearance of these rail language
    2.47 +  elements is illustrated by the following representative examples.
    2.48 +
    2.49 +  \begin{itemize}
    2.50 +
    2.51 +  \item Empty @{verbatim "()"}
    2.52 +
    2.53 +  @{rail "()"}
    2.54 +
    2.55 +  \item Nonterminal @{verbatim "A"}
    2.56 +
    2.57 +  @{rail "A"}
    2.58 +
    2.59 +  \item Nonterminal via Isabelle antiquotation
    2.60 +  @{verbatim "@{syntax method}"}
    2.61 +
    2.62 +  @{rail "@{syntax method}"}
    2.63 +
    2.64 +  \item Terminal @{verbatim "'xyz'"}
    2.65 +
    2.66 +  @{rail "'xyz'"}
    2.67 +
    2.68 +  \item Terminal in keyword style @{verbatim "@'xyz'"}
    2.69 +
    2.70 +  @{rail "@'xyz'"}
    2.71 +
    2.72 +  \item Terminal via Isabelle antiquotation
    2.73 +  @{verbatim "@@{method rule}"}
    2.74 +
    2.75 +  @{rail "@@{method rule}"}
    2.76 +
    2.77 +  \item Concatenation @{verbatim "A B C"}
    2.78 +
    2.79 +  @{rail "A B C"}
    2.80 +
    2.81 +  \item Linebreak @{verbatim "\\\\"} inside
    2.82 +  concatenation\footnote{Strictly speaking, this is only a single
    2.83 +  backslash, but the enclosing @{syntax string} syntax requires a
    2.84 +  second one for escaping.} @{verbatim "A B C \\\\ D E F"}
    2.85 +
    2.86 +  @{rail "A B C \\ D E F"}
    2.87 +
    2.88 +  \item Variants @{verbatim "A | B | C"}
    2.89 +
    2.90 +  @{rail "A | B | C"}
    2.91 +
    2.92 +  \item Option @{verbatim "A ?"}
    2.93 +
    2.94 +  @{rail "A ?"}
    2.95 +
    2.96 +  \item Repetition @{verbatim "A *"}
    2.97 +
    2.98 +  @{rail "A *"}
    2.99 +
   2.100 +  \item Repetition with separator @{verbatim "A * sep"}
   2.101 +
   2.102 +  @{rail "A * sep"}
   2.103 +
   2.104 +  \item Strict repetition @{verbatim "A +"}
   2.105 +
   2.106 +  @{rail "A +"}
   2.107 +
   2.108 +  \item Strict repetition with separator @{verbatim "A + sep"}
   2.109 +
   2.110 +  @{rail "A + sep"}
   2.111 +
   2.112 +  \end{itemize}
   2.113 +*}
   2.114 +
   2.115 +
   2.116  section {* Draft presentation *}
   2.117  
   2.118  text {*

     3.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 17:31:16 2011 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex	Tue May 03 18:04:05 2011 +0200
     3.3 @@ -632,6 +632,289 @@
     3.4  \end{isamarkuptext}%
     3.5  \isamarkuptrue%
     3.6  %
     3.7 +\isamarkupsection{Railroad diagrams%
     3.8 +}
     3.9 +\isamarkuptrue%
    3.10 +%
    3.11 +\begin{isamarkuptext}%
    3.12 +\begin{matharray}{rcl}
    3.13 +    \indexdef{}{antiquotation}{rail}\hypertarget{antiquotation.rail}{\hyperlink{antiquotation.rail}{\mbox{\isa{rail}}}} & : & \isa{antiquotation} \\
    3.14 +  \end{matharray}
    3.15 +
    3.16 +  \begin{railoutput}
    3.17 +\rail@begin{1}{\isa{}}
    3.18 +\rail@term{\isa{rail}}[]
    3.19 +\rail@nont{\isa{string}}[]
    3.20 +\rail@end
    3.21 +\end{railoutput}
    3.22 +
    3.23 +
    3.24 +  The \hyperlink{antiquotation.rail}{\mbox{\isa{rail}}} antiquotation allows to include syntax
    3.25 +  diagrams into Isabelle documents.  {\LaTeX} requires the style file
    3.26 +  \verb|~~/lib/texinputs/pdfsetup.sty|, which can be used via
    3.27 +  \verb|\usepackage{pdfsetup}| in \verb|root.tex|, for
    3.28 +  example.
    3.29 +
    3.30 +  The rail specification language is quoted here as Isabelle \hyperlink{syntax.string}{\mbox{\isa{string}}}; it has its own grammar given below.
    3.31 +
    3.32 +  \begin{railoutput}
    3.33 +\rail@begin{3}{\isa{}}
    3.34 +\rail@plus
    3.35 +\rail@bar
    3.36 +\rail@nextbar{1}
    3.37 +\rail@nont{\isa{rule}}[]
    3.38 +\rail@endbar
    3.39 +\rail@nextplus{2}
    3.40 +\rail@cterm{\isa{{\isaliteral{3B}{\isacharsemicolon}}}}[]
    3.41 +\rail@endplus
    3.42 +\rail@end
    3.43 +\rail@begin{3}{\isa{rule}}
    3.44 +\rail@bar
    3.45 +\rail@nextbar{1}
    3.46 +\rail@bar
    3.47 +\rail@nont{\isa{identifier}}[]
    3.48 +\rail@nextbar{2}
    3.49 +\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[]
    3.50 +\rail@endbar
    3.51 +\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
    3.52 +\rail@endbar
    3.53 +\rail@nont{\isa{body}}[]
    3.54 +\rail@end
    3.55 +\rail@begin{2}{\isa{body}}
    3.56 +\rail@plus
    3.57 +\rail@nont{\isa{concatenation}}[]
    3.58 +\rail@nextplus{1}
    3.59 +\rail@cterm{\isa{{\isaliteral{7C}{\isacharbar}}}}[]
    3.60 +\rail@endplus
    3.61 +\rail@end
    3.62 +\rail@begin{3}{\isa{concatenation}}
    3.63 +\rail@plus
    3.64 +\rail@nont{\isa{atom}}[]
    3.65 +\rail@bar
    3.66 +\rail@nextbar{1}
    3.67 +\rail@term{\isa{{\isaliteral{3F}{\isacharquery}}}}[]
    3.68 +\rail@endbar
    3.69 +\rail@nextplus{2}
    3.70 +\rail@endplus
    3.71 +\rail@bar
    3.72 +\rail@nextbar{1}
    3.73 +\rail@bar
    3.74 +\rail@term{\isa{{\isaliteral{2A}{\isacharasterisk}}}}[]
    3.75 +\rail@nextbar{2}
    3.76 +\rail@term{\isa{{\isaliteral{2B}{\isacharplus}}}}[]
    3.77 +\rail@endbar
    3.78 +\rail@bar
    3.79 +\rail@nextbar{2}
    3.80 +\rail@nont{\isa{atom}}[]
    3.81 +\rail@endbar
    3.82 +\rail@endbar
    3.83 +\rail@end
    3.84 +\rail@begin{6}{\isa{atom}}
    3.85 +\rail@bar
    3.86 +\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
    3.87 +\rail@bar
    3.88 +\rail@nextbar{1}
    3.89 +\rail@nont{\isa{body}}[]
    3.90 +\rail@endbar
    3.91 +\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
    3.92 +\rail@nextbar{2}
    3.93 +\rail@nont{\isa{identifier}}[]
    3.94 +\rail@nextbar{3}
    3.95 +\rail@bar
    3.96 +\rail@nextbar{4}
    3.97 +\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[]
    3.98 +\rail@endbar
    3.99 +\rail@bar
   3.100 +\rail@nont{\isa{string}}[]
   3.101 +\rail@nextbar{4}
   3.102 +\rail@nont{\hyperlink{syntax.antiquotation}{\mbox{\isa{antiquotation}}}}[]
   3.103 +\rail@endbar
   3.104 +\rail@nextbar{5}
   3.105 +\rail@term{\isa{{\isaliteral{5C}{\isacharbackslash}}{\isaliteral{5C}{\isacharbackslash}}}}[]
   3.106 +\rail@endbar
   3.107 +\rail@end
   3.108 +\end{railoutput}
   3.109 +
   3.110 +
   3.111 +  The lexical syntax of \isa{{\isaliteral{22}{\isachardoublequote}}identifier{\isaliteral{22}{\isachardoublequote}}} coincides with that of
   3.112 +  \hyperlink{syntax.ident}{\mbox{\isa{ident}}} in regular Isabelle syntax, but \isa{string} uses
   3.113 +  single quotes instead of double quotes of the standard \hyperlink{syntax.string}{\mbox{\isa{string}}} category, to avoid extra escapes.
   3.114 +
   3.115 +  Each \isa{rule} defines a formal language (with optional name),
   3.116 +  using a notation that is similar to EBNF or regular expressions with
   3.117 +  recursion.  The meaning and visual appearance of these rail language
   3.118 +  elements is illustrated by the following representative examples.
   3.119 +
   3.120 +  \begin{itemize}
   3.121 +
   3.122 +  \item Empty \verb|()|
   3.123 +
   3.124 +  \begin{railoutput}
   3.125 +\rail@begin{1}{\isa{}}
   3.126 +\rail@end
   3.127 +\end{railoutput}
   3.128 +
   3.129 +
   3.130 +  \item Nonterminal \verb|A|
   3.131 +
   3.132 +  \begin{railoutput}
   3.133 +\rail@begin{1}{\isa{}}
   3.134 +\rail@nont{\isa{A}}[]
   3.135 +\rail@end
   3.136 +\end{railoutput}
   3.137 +
   3.138 +
   3.139 +  \item Nonterminal via Isabelle antiquotation
   3.140 +  \verb|@{syntax method}|
   3.141 +
   3.142 +  \begin{railoutput}
   3.143 +\rail@begin{1}{\isa{}}
   3.144 +\rail@nont{\hyperlink{syntax.method}{\mbox{\isa{method}}}}[]
   3.145 +\rail@end
   3.146 +\end{railoutput}
   3.147 +
   3.148 +
   3.149 +  \item Terminal \verb|'xyz'|
   3.150 +
   3.151 +  \begin{railoutput}
   3.152 +\rail@begin{1}{\isa{}}
   3.153 +\rail@term{\isa{xyz}}[]
   3.154 +\rail@end
   3.155 +\end{railoutput}
   3.156 +
   3.157 +
   3.158 +  \item Terminal in keyword style \verb|@'xyz'|
   3.159 +
   3.160 +  \begin{railoutput}
   3.161 +\rail@begin{1}{\isa{}}
   3.162 +\rail@term{\isa{\isakeyword{xyz}}}[]
   3.163 +\rail@end
   3.164 +\end{railoutput}
   3.165 +
   3.166 +
   3.167 +  \item Terminal via Isabelle antiquotation
   3.168 +  \verb|@@{method rule}|
   3.169 +
   3.170 +  \begin{railoutput}
   3.171 +\rail@begin{1}{\isa{}}
   3.172 +\rail@term{\hyperlink{method.rule}{\mbox{\isa{rule}}}}[]
   3.173 +\rail@end
   3.174 +\end{railoutput}
   3.175 +
   3.176 +
   3.177 +  \item Concatenation \verb|A B C|
   3.178 +
   3.179 +  \begin{railoutput}
   3.180 +\rail@begin{1}{\isa{}}
   3.181 +\rail@nont{\isa{A}}[]
   3.182 +\rail@nont{\isa{B}}[]
   3.183 +\rail@nont{\isa{C}}[]
   3.184 +\rail@end
   3.185 +\end{railoutput}
   3.186 +
   3.187 +
   3.188 +  \item Linebreak \verb|\\| inside
   3.189 +  concatenation\footnote{Strictly speaking, this is only a single
   3.190 +  backslash, but the enclosing \hyperlink{syntax.string}{\mbox{\isa{string}}} syntax requires a
   3.191 +  second one for escaping.} \verb|A B C \\ D E F|
   3.192 +
   3.193 +  \begin{railoutput}
   3.194 +\rail@begin{3}{\isa{}}
   3.195 +\rail@nont{\isa{A}}[]
   3.196 +\rail@nont{\isa{B}}[]
   3.197 +\rail@nont{\isa{C}}[]
   3.198 +\rail@cr{2}
   3.199 +\rail@nont{\isa{D}}[]
   3.200 +\rail@nont{\isa{E}}[]
   3.201 +\rail@nont{\isa{F}}[]
   3.202 +\rail@end
   3.203 +\end{railoutput}
   3.204 +
   3.205 +
   3.206 +  \item Variants \verb|A |\verb,|,\verb| B |\verb,|,\verb| C|
   3.207 +
   3.208 +  \begin{railoutput}
   3.209 +\rail@begin{3}{\isa{}}
   3.210 +\rail@bar
   3.211 +\rail@nont{\isa{A}}[]
   3.212 +\rail@nextbar{1}
   3.213 +\rail@nont{\isa{B}}[]
   3.214 +\rail@nextbar{2}
   3.215 +\rail@nont{\isa{C}}[]
   3.216 +\rail@endbar
   3.217 +\rail@end
   3.218 +\end{railoutput}
   3.219 +
   3.220 +
   3.221 +  \item Option \verb|A ?|
   3.222 +
   3.223 +  \begin{railoutput}
   3.224 +\rail@begin{2}{\isa{}}
   3.225 +\rail@bar
   3.226 +\rail@nextbar{1}
   3.227 +\rail@nont{\isa{A}}[]
   3.228 +\rail@endbar
   3.229 +\rail@end
   3.230 +\end{railoutput}
   3.231 +
   3.232 +
   3.233 +  \item Repetition \verb|A *|
   3.234 +
   3.235 +  \begin{railoutput}
   3.236 +\rail@begin{2}{\isa{}}
   3.237 +\rail@plus
   3.238 +\rail@nextplus{1}
   3.239 +\rail@cnont{\isa{A}}[]
   3.240 +\rail@endplus
   3.241 +\rail@end
   3.242 +\end{railoutput}
   3.243 +
   3.244 +
   3.245 +  \item Repetition with separator \verb|A * sep|
   3.246 +
   3.247 +  \begin{railoutput}
   3.248 +\rail@begin{3}{\isa{}}
   3.249 +\rail@bar
   3.250 +\rail@nextbar{1}
   3.251 +\rail@plus
   3.252 +\rail@nont{\isa{A}}[]
   3.253 +\rail@nextplus{2}
   3.254 +\rail@cnont{\isa{sep}}[]
   3.255 +\rail@endplus
   3.256 +\rail@endbar
   3.257 +\rail@end
   3.258 +\end{railoutput}
   3.259 +
   3.260 +
   3.261 +  \item Strict repetition \verb|A +|
   3.262 +
   3.263 +  \begin{railoutput}
   3.264 +\rail@begin{2}{\isa{}}
   3.265 +\rail@plus
   3.266 +\rail@nont{\isa{A}}[]
   3.267 +\rail@nextplus{1}
   3.268 +\rail@endplus
   3.269 +\rail@end
   3.270 +\end{railoutput}
   3.271 +
   3.272 +
   3.273 +  \item Strict repetition with separator \verb|A + sep|
   3.274 +
   3.275 +  \begin{railoutput}
   3.276 +\rail@begin{2}{\isa{}}
   3.277 +\rail@plus
   3.278 +\rail@nont{\isa{A}}[]
   3.279 +\rail@nextplus{1}
   3.280 +\rail@cnont{\isa{sep}}[]
   3.281 +\rail@endplus
   3.282 +\rail@end
   3.283 +\end{railoutput}
   3.284 +
   3.285 +
   3.286 +  \end{itemize}%
   3.287 +\end{isamarkuptext}%
   3.288 +\isamarkuptrue%
   3.289 +%
   3.290  \isamarkupsection{Draft presentation%
   3.291  }
   3.292  \isamarkuptrue%