# HG changeset patch
# User wenzelm
# Date 1304200919 -7200
# Node ID b9c1067633254e8c2a48bb616c5d2e4fa430e655
# Parent  9d107a52b6345eeb8f39f11ebafe6d3aa5bae4b3
use @{rail} antiquotation (with some nested markup);
eliminated separate rail/latex phase;

diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Makefile
--- a/doc-src/IsarImplementation/Makefile	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Makefile	Sun May 01 00:01:59 2011 +0200
@@ -22,7 +22,6 @@
 
 $(NAME).dvi: $(FILES) isabelle_isar.eps
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)
@@ -34,7 +33,6 @@
 
 $(NAME).pdf: $(FILES) isabelle_isar.pdf
 	$(PDFLATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(PDFLATEX) $(NAME)
 	$(PDFLATEX) $(NAME)
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Sun May 01 00:01:59 2011 +0200
@@ -197,16 +197,17 @@
   @{ML_antiquotation_def "typ"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'class' nameref
+  @{rail "
+  @@{ML_antiquotation class} nameref
   ;
-  'sort' sort
+  @@{ML_antiquotation sort} sort
   ;
-  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
+  (@@{ML_antiquotation type_name} |
+   @@{ML_antiquotation type_abbrev} |
+   @@{ML_antiquotation nonterminal}) nameref
   ;
-  'typ' type
-  ;
-  \end{rail}
+  @@{ML_antiquotation typ} type
+  "}
 
   \begin{description}
 
@@ -436,16 +437,16 @@
   @{ML_antiquotation_def "prop"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  ('const_name' | 'const_abbrev') nameref
-  ;
-  'const' ('(' (type + ',') ')')?
+  @{rail "
+  (@@{ML_antiquotation const_name} |
+   @@{ML_antiquotation const_abbrev}) nameref
   ;
-  'term' term
+  @@{ML_antiquotation const} ('(' (type + ',') ')')?
   ;
-  'prop' prop
+  @@{ML_antiquotation term} term
   ;
-  \end{rail}
+  @@{ML_antiquotation prop} prop
+  "}
 
   \begin{description}
 
@@ -733,19 +734,20 @@
   @{ML_antiquotation_def "lemma"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'ctyp' typ
+  @{rail "
+  @@{ML_antiquotation ctyp} typ
   ;
-  'cterm' term
+  @@{ML_antiquotation cterm} term
   ;
-  'cprop' prop
+  @@{ML_antiquotation cprop} prop
   ;
-  'thm' thmref
+  @@{ML_antiquotation thm} thmref
+  ;
+  @@{ML_antiquotation thms} thmrefs
   ;
-  'thms' thmrefs
-  ;
-  'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method?
-  \end{rail}
+  @@{ML_antiquotation lemma} ('(' @@{keyword \"open\"} ')')? ((prop +) + @@{keyword \"and\"}) \\
+    @@{keyword \"by\"} method method?
+  "}
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Sun May 01 00:01:59 2011 +0200
@@ -666,11 +666,9 @@
   concept of \emph{ML antiquotation}.  The standard token language of
   ML is augmented by special syntactic entities of the following form:
 
-  \indexouternonterm{antiquote}
-  \begin{rail}
-  antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
-  ;
-  \end{rail}
+  @{rail "
+  @{syntax_def antiquote}: '@' '{' nameref args '}' | '\<lbrace>' | '\<rbrace>'
+  "}
 
   Here @{syntax nameref} and @{syntax args} are regular outer syntax
   categories \cite{isabelle-isar-ref}.  Attributes and proof methods
@@ -700,13 +698,11 @@
   @{ML_antiquotation_def "note"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'let' ((term + 'and') '=' term + 'and')
+  @{rail "
+  @@{ML_antiquotation let} ((term + @@{keyword \"and\"}) '=' term + @@{keyword \"and\"})
   ;
-
-  'note' (thmdef? thmrefs + 'and')
-  ;
-  \end{rail}
+  @@{ML_antiquotation note} (thmdef? thmrefs + @@{keyword \"and\"})
+  "}
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sun May 01 00:01:59 2011 +0200
@@ -228,10 +228,9 @@
   @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'theory' nameref?
-  ;
-  \end{rail}
+  @{rail "
+  @@{ML_antiquotation theory} nameref?
+  "}
 
   \begin{description}
 
@@ -1205,10 +1204,9 @@
   @{ML_antiquotation_def "binding"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'binding' name
-  ;
-  \end{rail}
+  @{rail "
+  @@{ML_antiquotation binding} name
+  "}
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/Syntax.thy
--- a/doc-src/IsarImplementation/Thy/Syntax.thy	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Syntax.thy	Sun May 01 00:01:59 2011 +0200
@@ -81,10 +81,12 @@
   @{ML_antiquotation_def "syntax_const"} & : & @{text ML_antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
-  ;
-  \end{rail}
+  @{rail "
+  (@@{ML_antiquotation class_syntax} |
+   @@{ML_antiquotation type_syntax} |
+   @@{ML_antiquotation const_syntax} |
+   @@{ML_antiquotation syntax_const}) name
+  "}
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Sun May 01 00:01:59 2011 +0200
@@ -216,16 +216,31 @@
   \indexdef{}{ML antiquotation}{typ}\hypertarget{ML antiquotation.typ}{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'class' nameref
-  ;
-  'sort' sort
-  ;
-  ('type_name' | 'type_abbrev' | 'nonterminal') nameref
-  ;
-  'typ' type
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.class}{\mbox{\isa{class}}}}[]
+\rail@nont{\isa{nameref}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.sort}{\mbox{\isa{sort}}}}[]
+\rail@nont{\isa{sort}}[]
+\rail@end
+\rail@begin{3}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{ML antiquotation.type-name}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{ML antiquotation.type-abbrev}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{ML antiquotation.nonterminal}{\mbox{\isa{nonterminal}}}}[]
+\rail@endbar
+\rail@nont{\isa{nameref}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.typ}{\mbox{\isa{typ}}}}[]
+\rail@nont{\isa{type}}[]
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
 
@@ -465,16 +480,38 @@
   \indexdef{}{ML antiquotation}{prop}\hypertarget{ML antiquotation.prop}{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  ('const_name' | 'const_abbrev') nameref
-  ;
-  'const' ('(' (type + ',') ')')?
-  ;
-  'term' term
-  ;
-  'prop' prop
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{ML antiquotation.const-name}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}name}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{ML antiquotation.const-abbrev}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}abbrev}}}}[]
+\rail@endbar
+\rail@nont{\isa{nameref}}[]
+\rail@end
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.const}{\mbox{\isa{const}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@plus
+\rail@nont{\isa{type}}[]
+\rail@nextplus{2}
+\rail@cterm{\isa{{\isaliteral{2C}{\isacharcomma}}}}[]
+\rail@endplus
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.term}{\mbox{\isa{term}}}}[]
+\rail@nont{\isa{term}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.prop}{\mbox{\isa{prop}}}}[]
+\rail@nont{\isa{prop}}[]
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
 
@@ -775,19 +812,53 @@
   \indexdef{}{ML antiquotation}{lemma}\hypertarget{ML antiquotation.lemma}{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'ctyp' typ
-  ;
-  'cterm' term
-  ;
-  'cprop' prop
-  ;
-  'thm' thmref
-  ;
-  'thms' thmrefs
-  ;
-  'lemma' ('(open)')? ((prop +) + 'and') \\ 'by' method method?
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.ctyp}{\mbox{\isa{ctyp}}}}[]
+\rail@nont{\isa{typ}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.cterm}{\mbox{\isa{cterm}}}}[]
+\rail@nont{\isa{term}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.cprop}{\mbox{\isa{cprop}}}}[]
+\rail@nont{\isa{prop}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.thm}{\mbox{\isa{thm}}}}[]
+\rail@nont{\isa{thmref}}[]
+\rail@end
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.thms}{\mbox{\isa{thms}}}}[]
+\rail@nont{\isa{thmrefs}}[]
+\rail@end
+\rail@begin{6}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.lemma}{\mbox{\isa{lemma}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
+\rail@term{\hyperlink{keyword.open}{\mbox{\isa{\isakeyword{open}}}}}[]
+\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
+\rail@endbar
+\rail@plus
+\rail@plus
+\rail@nont{\isa{prop}}[]
+\rail@nextplus{1}
+\rail@endplus
+\rail@nextplus{2}
+\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@endplus
+\rail@cr{4}
+\rail@term{\hyperlink{keyword.by}{\mbox{\isa{\isakeyword{by}}}}}[]
+\rail@nont{\isa{method}}[]
+\rail@bar
+\rail@nextbar{5}
+\rail@nont{\isa{method}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/document/ML.tex
--- a/doc-src/IsarImplementation/Thy/document/ML.tex	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex	Sun May 01 00:01:59 2011 +0200
@@ -796,11 +796,22 @@
   concept of \emph{ML antiquotation}.  The standard token language of
   ML is augmented by special syntactic entities of the following form:
 
-  \indexouternonterm{antiquote}
-  \begin{rail}
-  antiquote: atsign lbrace nameref args rbrace | lbracesym | rbracesym
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{3}{\indexdef{}{syntax}{antiquote}\hypertarget{syntax.antiquote}{\hyperlink{syntax.antiquote}{\mbox{\isa{antiquote}}}}}
+\rail@bar
+\rail@term{\isa{{\isaliteral{40}{\isacharat}}}}[]
+\rail@term{\isa{{\isaliteral{7B}{\isacharbraceleft}}}}[]
+\rail@nont{\isa{nameref}}[]
+\rail@nont{\isa{args}}[]
+\rail@term{\isa{{\isaliteral{7D}{\isacharbraceright}}}}[]
+\rail@nextbar{1}
+\rail@term{\isa{{\isaliteral{5C3C6C62726163653E}{\isasymlbrace}}}}[]
+\rail@nextbar{2}
+\rail@term{\isa{{\isaliteral{5C3C7262726163653E}{\isasymrbrace}}}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
 
   Here \hyperlink{syntax.nameref}{\mbox{\isa{nameref}}} and \hyperlink{syntax.args}{\mbox{\isa{args}}} are regular outer syntax
   categories \cite{isabelle-isar-ref}.  Attributes and proof methods
@@ -837,13 +848,35 @@
   \indexdef{}{ML antiquotation}{note}\hypertarget{ML antiquotation.note}{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'let' ((term + 'and') '=' term + 'and')
-  ;
+  \begin{railoutput}
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.let}{\mbox{\isa{let}}}}[]
+\rail@plus
+\rail@plus
+\rail@nont{\isa{term}}[]
+\rail@nextplus{1}
+\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@endplus
+\rail@term{\isa{{\isaliteral{3D}{\isacharequal}}}}[]
+\rail@nont{\isa{term}}[]
+\rail@nextplus{2}
+\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@endplus
+\rail@end
+\rail@begin{3}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.note}{\mbox{\isa{note}}}}[]
+\rail@plus
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{thmdef}}[]
+\rail@endbar
+\rail@nont{\isa{thmrefs}}[]
+\rail@nextplus{2}
+\rail@cterm{\hyperlink{keyword.and}{\mbox{\isa{\isakeyword{and}}}}}[]
+\rail@endplus
+\rail@end
+\end{railoutput}
 
-  'note' (thmdef? thmrefs + 'and')
-  ;
-  \end{rail}
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/document/Prelim.tex
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sun May 01 00:01:59 2011 +0200
@@ -264,10 +264,16 @@
   \indexdef{}{ML antiquotation}{theory}\hypertarget{ML antiquotation.theory}{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'theory' nameref?
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{2}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.theory}{\mbox{\isa{theory}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\isa{nameref}}[]
+\rail@endbar
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
 
@@ -1711,10 +1717,13 @@
   \indexdef{}{ML antiquotation}{binding}\hypertarget{ML antiquotation.binding}{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  'binding' name
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{1}{\isa{}}
+\rail@term{\hyperlink{ML antiquotation.binding}{\mbox{\isa{binding}}}}[]
+\rail@nont{\isa{name}}[]
+\rail@end
+\end{railoutput}
+
 
   \begin{description}
 
diff -r 9d107a52b634 -r b9c106763325 doc-src/IsarImplementation/Thy/document/Syntax.tex
--- a/doc-src/IsarImplementation/Thy/document/Syntax.tex	Sat Apr 30 23:27:57 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Syntax.tex	Sun May 01 00:01:59 2011 +0200
@@ -167,10 +167,21 @@
   \indexdef{}{ML antiquotation}{syntax\_const}\hypertarget{ML antiquotation.syntax-const}{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}} & : & \isa{ML{\isaliteral{5F}{\isacharunderscore}}antiquotation} \\
   \end{matharray}
 
-  \begin{rail}
-  ('class_syntax' | 'type_syntax' | 'const_syntax' | 'syntax_const') name
-  ;
-  \end{rail}
+  \begin{railoutput}
+\rail@begin{4}{\isa{}}
+\rail@bar
+\rail@term{\hyperlink{ML antiquotation.class-syntax}{\mbox{\isa{class{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{1}
+\rail@term{\hyperlink{ML antiquotation.type-syntax}{\mbox{\isa{type{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{2}
+\rail@term{\hyperlink{ML antiquotation.const-syntax}{\mbox{\isa{const{\isaliteral{5F}{\isacharunderscore}}syntax}}}}[]
+\rail@nextbar{3}
+\rail@term{\hyperlink{ML antiquotation.syntax-const}{\mbox{\isa{syntax{\isaliteral{5F}{\isacharunderscore}}const}}}}[]
+\rail@endbar
+\rail@nont{\isa{name}}[]
+\rail@end
+\end{railoutput}
+
 
   \begin{description}