# HG changeset patch
# User wenzelm
# Date 1459253006 -7200
# Node ID aa0084adce1f024171788f808503a28b2a0f65a9
# Parent  fe827c6fa8c51de6fdf92de572414942667b1c64
tuned signature;

diff -r fe827c6fa8c5 -r aa0084adce1f src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Mon Mar 28 12:11:54 2016 +0200
+++ b/src/Pure/Tools/rail.ML	Tue Mar 29 14:03:26 2016 +0200
@@ -5,7 +5,22 @@
 Railroad diagrams in LaTeX.
 *)
 
-structure Rail: sig end =
+signature RAIL =
+sig
+  datatype rails =
+    Cat of int * rail list
+  and rail =
+    Bar of rails list |
+    Plus of rails * rails |
+    Newline of int |
+    Nonterminal of string |
+    Terminal of bool * string |
+    Antiquote of bool * Antiquote.antiq
+  val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
+  val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
+end;
+
+structure Rail: RAIL =
 struct
 
 (** lexical syntax **)
@@ -313,6 +328,8 @@
   | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   | vertical_range atom y = (atom, y + 1);
 
+in
+
 fun output_rules state rules =
   let
     val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
@@ -356,8 +373,6 @@
       end;
   in Latex.environment "railoutput" (implode (map output_rule rules)) end;
 
-in
-
 val _ = Theory.setup
   (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
     (fn {state, context, ...} => output_rules state o read context));
@@ -365,4 +380,3 @@
 end;
 
 end;
-