# 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%