1.1 --- a/doc-src/rail.ML	Mon Jul 27 23:17:40 2009 +0200
     1.2 +++ b/doc-src/rail.ML	Tue Jul 28 00:27:58 2009 +0200
     1.3 @@ -1,3 +1,12 @@
     1.4 +(*  Title:      doc-src/rail.ML
     1.5 +    Author:     Michael Kerscher, TUM
     1.6 +
     1.7 +Railroad diagrams for LaTeX.
     1.8 +*)
     1.9 +
    1.10 +structure Rail =
    1.11 +struct
    1.12 +
    1.13  datatype token =
    1.14    Identifier of string |
    1.15    Special_Identifier of string |
    1.16 @@ -9,7 +18,7 @@
    1.17  fun is_identifier (Identifier _) = true
    1.18    | is_identifier (Special_Identifier _ ) = true
    1.19    | is_identifier _ = false;
    1.20 -  
    1.21 +
    1.22  fun is_text (Text _) = true
    1.23    | is_text _ = false;
    1.24  
    1.25 @@ -65,7 +74,7 @@
    1.26    ("executable", ("isatt", no_check, true)),
    1.27    ("tool", ("isatt", K check_tool, true)),
    1.28    ("file", ("isatt", K (File.exists o Path.explode), true)),
    1.29 -  ("theory", ("", K ThyInfo.known_thy, true)) 
    1.30 +  ("theory", ("", K ThyInfo.known_thy, true))
    1.31    ];
    1.32  
    1.33  in
    1.34 @@ -123,7 +132,7 @@
    1.35  end;
    1.36  
    1.37  (* escaped version *)
    1.38 -fun scan_identifier ctxt = 
    1.39 +fun scan_identifier ctxt =
    1.40    let fun is_identifier_start s =
    1.41      Symbol.is_letter s orelse
    1.42      s = "_"
    1.43 @@ -197,13 +206,13 @@
    1.44    CR | EMPTY | ANNOTE | IDENT | STRING |
    1.45    Null_Kind;
    1.46  
    1.47 -datatype body_type =	
    1.48 +datatype body_type =
    1.49    Body of body_kind * string * string * id_type * body_type list |
    1.50    Body_Pos of body_kind * string * string * id_type * body_type list * int * int |
    1.51    Empty_Body |
    1.52    Null_Body;
    1.53  
    1.54 -datatype rule = 
    1.55 +datatype rule =
    1.56    Rule of id_type * body_type;
    1.57  
    1.58  fun new_id id kind = Id (id, kind);
    1.59 @@ -219,7 +228,7 @@
    1.60  fun add_list (Body(kind, text, annot, id, bodies), body) =
    1.61    Body(kind, text, annot, id, bodies @ [body]);
    1.62  
    1.63 -fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) = 
    1.64 +fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) =
    1.65        Body(kind, text, annot, id, bodies1 @ bodies2);
    1.66  
    1.67  fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =
    1.68 @@ -299,7 +308,7 @@
    1.69  	add_body(PLUS, new_empty_body, rev_body body1)
    1.70        else
    1.71  	add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
    1.72 -  parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >> 
    1.73 +  parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
    1.74      (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
    1.75    parse_body2e
    1.76    ) x
    1.77 @@ -326,7 +335,7 @@
    1.78    (
    1.79    $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||
    1.80    Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
    1.81 -    (fn (text, anot) => new_text_annote_body (text,anot)) ||    
    1.82 +    (fn (text, anot) => new_text_annote_body (text,anot)) ||
    1.83    Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
    1.84      (fn (id, anot) => new_ident_body (id,anot)) ||
    1.85    $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))
    1.86 @@ -401,7 +410,7 @@
    1.87      in
    1.88        format_bodies(bodies)
    1.89      end
    1.90 -  | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) = 
    1.91 +  | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
    1.92      let fun format_bodies([]) = "\\rail@endbar\n"
    1.93  	  | format_bodies(x::xs) =
    1.94  	      "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
    1.95 @@ -466,3 +475,6 @@
    1.96  
    1.97  val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
    1.98    (fn {context = ctxt,...} => fn txt => process txt ctxt);
    1.99 +
   1.100 +end;
   1.101 +