# HG changeset patch
# User wenzelm
# Date 1248733908 -7200
# Node ID 8467626b394e8a2a266e136e4a978dd9e30b5dc7
# Parent  a60f183eb63edd4a7dfca6116f97ff551ba81fb9# Parent  96345b9181258ec1b1bb5115a8be6dd22988d6ee
merged

diff -r a60f183eb63e -r 8467626b394e doc-src/rail.ML
--- a/doc-src/rail.ML	Mon Jul 27 23:43:35 2009 +0200
+++ b/doc-src/rail.ML	Tue Jul 28 00:31:48 2009 +0200
@@ -1,3 +1,12 @@
+(*  Title:      doc-src/rail.ML
+    Author:     Michael Kerscher, TUM
+
+Railroad diagrams for LaTeX.
+*)
+
+structure Rail =
+struct
+
 datatype token =
   Identifier of string |
   Special_Identifier of string |
@@ -9,7 +18,7 @@
 fun is_identifier (Identifier _) = true
   | is_identifier (Special_Identifier _ ) = true
   | is_identifier _ = false;
-  
+
 fun is_text (Text _) = true
   | is_text _ = false;
 
@@ -65,7 +74,7 @@
   ("executable", ("isatt", no_check, true)),
   ("tool", ("isatt", K check_tool, true)),
   ("file", ("isatt", K (File.exists o Path.explode), true)),
-  ("theory", ("", K ThyInfo.known_thy, true)) 
+  ("theory", ("", K ThyInfo.known_thy, true))
   ];
 
 in
@@ -123,7 +132,7 @@
 end;
 
 (* escaped version *)
-fun scan_identifier ctxt = 
+fun scan_identifier ctxt =
   let fun is_identifier_start s =
     Symbol.is_letter s orelse
     s = "_"
@@ -197,13 +206,13 @@
   CR | EMPTY | ANNOTE | IDENT | STRING |
   Null_Kind;
 
-datatype body_type =	
+datatype body_type =
   Body of body_kind * string * string * id_type * body_type list |
   Body_Pos of body_kind * string * string * id_type * body_type list * int * int |
   Empty_Body |
   Null_Body;
 
-datatype rule = 
+datatype rule =
   Rule of id_type * body_type;
 
 fun new_id id kind = Id (id, kind);
@@ -219,7 +228,7 @@
 fun add_list (Body(kind, text, annot, id, bodies), body) =
   Body(kind, text, annot, id, bodies @ [body]);
 
-fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) = 
+fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) =
       Body(kind, text, annot, id, bodies1 @ bodies2);
 
 fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =
@@ -299,7 +308,7 @@
 	add_body(PLUS, new_empty_body, rev_body body1)
       else
 	add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
-  parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >> 
+  parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
     (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
   parse_body2e
   ) x
@@ -326,7 +335,7 @@
   (
   $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||
   Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
-    (fn (text, anot) => new_text_annote_body (text,anot)) ||    
+    (fn (text, anot) => new_text_annote_body (text,anot)) ||
   Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
     (fn (id, anot) => new_ident_body (id,anot)) ||
   $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))
@@ -401,7 +410,7 @@
     in
       format_bodies(bodies)
     end
-  | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) = 
+  | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
     let fun format_bodies([]) = "\\rail@endbar\n"
 	  | format_bodies(x::xs) =
 	      "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
@@ -466,3 +475,6 @@
 
 val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
   (fn {context = ctxt,...} => fn txt => process txt ctxt);
+
+end;
+
diff -r a60f183eb63e -r 8467626b394e doc-src/railsetup.sty
--- a/doc-src/railsetup.sty	Mon Jul 27 23:43:35 2009 +0200
+++ b/doc-src/railsetup.sty	Tue Jul 28 00:31:48 2009 +0200
@@ -1,10 +1,4 @@
-
-\railalias{percent}{\%}
-\railalias{ppercent}{\%\%}
-\railalias{underscore}{\_}
-\railalias{lbrace}{\texttt{\ttlbrace}}
-\railalias{rbrace}{\texttt{\ttrbrace}}
-\railalias{atsign}{{\at}}
+%% dimensions
 
 \setlength\railextra{3.6ex}
 \setlength\railboxleft{0.9ex}
@@ -20,6 +14,22 @@
 \setlength\railtextup{5pt}
 \setlength\railjoinsize{16pt}
 
+
+%% rail antiquotation environment
+
+\newenvironment{railoutput}%
+{\begin{list}{}{\rail@param}\def\rail@expand{\relax}\makeatletter}{\end{list}}
+
+
+%% old-style content markup
+
+\railalias{percent}{\%}
+\railalias{ppercent}{\%\%}
+\railalias{underscore}{\_}
+\railalias{lbrace}{\texttt{\ttlbrace}}
+\railalias{rbrace}{\texttt{\ttrbrace}}
+\railalias{atsign}{{\at}}
+
 \def\rail@termfont{\small\ttfamily\upshape}
 \def\rail@tokenfont{\small\ttfamily\upshape}
 \def\rail@nontfont{\small\rmfamily\upshape}