src/Pure/Tools/rail.ML
changeset 62748 aa0084adce1f
parent 61476 1884c40f1539
child 62797 e08c44eed27f
     1.1 --- a/src/Pure/Tools/rail.ML	Mon Mar 28 12:11:54 2016 +0200
     1.2 +++ b/src/Pure/Tools/rail.ML	Tue Mar 29 14:03:26 2016 +0200
     1.3 @@ -5,7 +5,22 @@
     1.4  Railroad diagrams in LaTeX.
     1.5  *)
     1.6  
     1.7 -structure Rail: sig end =
     1.8 +signature RAIL =
     1.9 +sig
    1.10 +  datatype rails =
    1.11 +    Cat of int * rail list
    1.12 +  and rail =
    1.13 +    Bar of rails list |
    1.14 +    Plus of rails * rails |
    1.15 +    Newline of int |
    1.16 +    Nonterminal of string |
    1.17 +    Terminal of bool * string |
    1.18 +    Antiquote of bool * Antiquote.antiq
    1.19 +  val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
    1.20 +  val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
    1.21 +end;
    1.22 +
    1.23 +structure Rail: RAIL =
    1.24  struct
    1.25  
    1.26  (** lexical syntax **)
    1.27 @@ -313,6 +328,8 @@
    1.28    | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
    1.29    | vertical_range atom y = (atom, y + 1);
    1.30  
    1.31 +in
    1.32 +
    1.33  fun output_rules state rules =
    1.34    let
    1.35      val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
    1.36 @@ -356,8 +373,6 @@
    1.37        end;
    1.38    in Latex.environment "railoutput" (implode (map output_rule rules)) end;
    1.39  
    1.40 -in
    1.41 -
    1.42  val _ = Theory.setup
    1.43    (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
    1.44      (fn {state, context, ...} => output_rules state o read context));
    1.45 @@ -365,4 +380,3 @@
    1.46  end;
    1.47  
    1.48  end;
    1.49 -