# HG changeset patch
# User wenzelm
# Date 1248733678 -7200
# Node ID 2b175fc6668a2b42792771997c9676812eb9efdf
# Parent  6c394343360f382d21507acd567eac9d8197ec9e
proper header;
proper structure;
tuned white space;

diff -r 6c394343360f -r 2b175fc6668a doc-src/rail.ML
--- a/doc-src/rail.ML	Mon Jul 27 23:17:40 2009 +0200
+++ b/doc-src/rail.ML	Tue Jul 28 00:27:58 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;
+