prefer user-space tool within Pure.thy;
authorwenzelm
Fri Jan 17 20:31:39 2014 +0100 (2014-01-17)
changeset 550309a9049d12e21
parent 55029 61a6bf7d4b02
child 55031 e58066daa065
prefer user-space tool within Pure.thy;
src/Pure/Pure.thy
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/rail.ML
src/Pure/Tools/rail.ML
     1.1 --- a/src/Pure/Pure.thy	Fri Jan 17 20:20:20 2014 +0100
     1.2 +++ b/src/Pure/Pure.thy	Fri Jan 17 20:31:39 2014 +0100
     1.3 @@ -103,6 +103,7 @@
     1.4  begin
     1.5  
     1.6  ML_file "Isar/isar_syn.ML"
     1.7 +ML_file "Tools/rail.ML"
     1.8  ML_file "Tools/rule_insts.ML";
     1.9  ML_file "Tools/find_theorems.ML"
    1.10  ML_file "Tools/find_consts.ML"
     2.1 --- a/src/Pure/ROOT	Fri Jan 17 20:20:20 2014 +0100
     2.2 +++ b/src/Pure/ROOT	Fri Jan 17 20:31:39 2014 +0100
     2.3 @@ -194,7 +194,6 @@
     2.4      "Thy/html.ML"
     2.5      "Thy/latex.ML"
     2.6      "Thy/present.ML"
     2.7 -    "Thy/rail.ML"
     2.8      "Thy/term_style.ML"
     2.9      "Thy/thm_deps.ML"
    2.10      "Thy/thy_header.ML"
     3.1 --- a/src/Pure/ROOT.ML	Fri Jan 17 20:20:20 2014 +0100
     3.2 +++ b/src/Pure/ROOT.ML	Fri Jan 17 20:31:39 2014 +0100
     3.3 @@ -281,7 +281,6 @@
     3.4  use "Thy/thy_load.ML";
     3.5  use "Thy/thy_info.ML";
     3.6  use "PIDE/document.ML";
     3.7 -use "Thy/rail.ML";
     3.8  
     3.9  (*theory and proof operations*)
    3.10  use "Thy/thm_deps.ML";
     4.1 --- a/src/Pure/Thy/rail.ML	Fri Jan 17 20:20:20 2014 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,275 +0,0 @@
     4.4 -(*  Title:      Pure/Thy/rail.ML
     4.5 -    Author:     Michael Kerscher, TU München
     4.6 -    Author:     Makarius
     4.7 -
     4.8 -Railroad diagrams in LaTeX.
     4.9 -*)
    4.10 -
    4.11 -structure Rail: sig end =
    4.12 -struct
    4.13 -
    4.14 -(** lexical syntax **)
    4.15 -
    4.16 -(* datatype token *)
    4.17 -
    4.18 -datatype kind =
    4.19 -  Keyword | Ident | String | Antiq of Symbol_Pos.T list * Position.range | EOF;
    4.20 -
    4.21 -datatype token = Token of Position.range * (kind * string);
    4.22 -
    4.23 -fun pos_of (Token ((pos, _), _)) = pos;
    4.24 -fun end_pos_of (Token ((_, pos), _)) = pos;
    4.25 -
    4.26 -fun kind_of (Token (_, (k, _))) = k;
    4.27 -fun content_of (Token (_, (_, x))) = x;
    4.28 -
    4.29 -
    4.30 -(* diagnostics *)
    4.31 -
    4.32 -val print_kind =
    4.33 - fn Keyword => "rail keyword"
    4.34 -  | Ident => "identifier"
    4.35 -  | String => "single-quoted string"
    4.36 -  | Antiq _ => "antiquotation"
    4.37 -  | EOF => "end-of-input";
    4.38 -
    4.39 -fun print (Token ((pos, _), (k, x))) =
    4.40 -  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
    4.41 -  Position.here pos;
    4.42 -
    4.43 -fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
    4.44 -
    4.45 -
    4.46 -(* stopper *)
    4.47 -
    4.48 -fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
    4.49 -val eof = mk_eof Position.none;
    4.50 -
    4.51 -fun is_eof (Token (_, (EOF, _))) = true
    4.52 -  | is_eof _ = false;
    4.53 -
    4.54 -val stopper =
    4.55 -  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
    4.56 -
    4.57 -
    4.58 -(* tokenize *)
    4.59 -
    4.60 -local
    4.61 -
    4.62 -fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
    4.63 -
    4.64 -val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    4.65 -
    4.66 -val scan_keyword =
    4.67 -  Scan.one
    4.68 -    (member (op =) ["|", "*", "+", "?", "(", ")", "\\<newline>", ";", ":", "@"] o Symbol_Pos.symbol);
    4.69 -
    4.70 -val err_prefix = "Rail lexical error: ";
    4.71 -
    4.72 -val scan_token =
    4.73 -  scan_space >> K [] ||
    4.74 -  Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
    4.75 -  scan_keyword >> (token Keyword o single) ||
    4.76 -  Lexicon.scan_id >> token Ident ||
    4.77 -  Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
    4.78 -
    4.79 -val scan =
    4.80 -  (Scan.repeat scan_token >> flat) --|
    4.81 -    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
    4.82 -      (Scan.ahead (Scan.one Symbol_Pos.is_eof));
    4.83 -
    4.84 -in
    4.85 -
    4.86 -val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
    4.87 -
    4.88 -end;
    4.89 -
    4.90 -
    4.91 -
    4.92 -(** parsing **)
    4.93 -
    4.94 -fun !!! scan =
    4.95 -  let
    4.96 -    val prefix = "Rail syntax error";
    4.97 -
    4.98 -    fun get_pos [] = " (end-of-input)"
    4.99 -      | get_pos (tok :: _) = Position.here (pos_of tok);
   4.100 -
   4.101 -    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
   4.102 -      | err (toks, SOME msg) =
   4.103 -          (fn () =>
   4.104 -            let val s = msg () in
   4.105 -              if String.isPrefix prefix s then s
   4.106 -              else prefix ^ get_pos toks ^ ": " ^ s
   4.107 -            end);
   4.108 -  in Scan.!! err scan end;
   4.109 -
   4.110 -fun $$$ x =
   4.111 -  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   4.112 -  Scan.fail_with
   4.113 -    (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
   4.114 -      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
   4.115 -
   4.116 -fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   4.117 -fun enum sep scan = enum1 sep scan || Scan.succeed [];
   4.118 -
   4.119 -val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
   4.120 -val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
   4.121 -
   4.122 -val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
   4.123 -
   4.124 -
   4.125 -
   4.126 -(** rail expressions **)
   4.127 -
   4.128 -(* datatype *)
   4.129 -
   4.130 -datatype rails =
   4.131 -  Cat of int * rail list
   4.132 -and rail =
   4.133 -  Bar of rails list |
   4.134 -  Plus of rails * rails |
   4.135 -  Newline of int |
   4.136 -  Nonterminal of string |
   4.137 -  Terminal of bool * string |
   4.138 -  Antiquote of bool * (Symbol_Pos.T list * Position.range);
   4.139 -
   4.140 -fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
   4.141 -and reverse (Bar cats) = Bar (map reverse_cat cats)
   4.142 -  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   4.143 -  | reverse x = x;
   4.144 -
   4.145 -fun cat rails = Cat (0, rails);
   4.146 -
   4.147 -val empty = cat [];
   4.148 -fun is_empty (Cat (_, [])) = true | is_empty _ = false;
   4.149 -
   4.150 -fun is_newline (Newline _) = true | is_newline _ = false;
   4.151 -
   4.152 -fun bar [Cat (_, [rail])] = rail
   4.153 -  | bar cats = Bar cats;
   4.154 -
   4.155 -fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
   4.156 -
   4.157 -fun star cat1 cat2 =
   4.158 -  if is_empty cat2 then plus empty cat1
   4.159 -  else bar [empty, cat [plus cat1 cat2]];
   4.160 -
   4.161 -fun maybe rail = bar [empty, cat [rail]];
   4.162 -
   4.163 -
   4.164 -(* read *)
   4.165 -
   4.166 -local
   4.167 -
   4.168 -val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
   4.169 -
   4.170 -fun body x = (enum1 "|" body1 >> bar) x
   4.171 -and body0 x = (enum "|" body1 >> bar) x
   4.172 -and body1 x =
   4.173 - (body2 :|-- (fn a =>
   4.174 -   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
   4.175 -   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
   4.176 -   Scan.succeed a)) x
   4.177 -and body2 x = (Scan.repeat1 body3 >> cat) x
   4.178 -and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
   4.179 -and body4 x =
   4.180 - ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   4.181 -  $$$ "\\<newline>" >> K (Newline 0) ||
   4.182 -  ident >> Nonterminal ||
   4.183 -  at_mode -- string >> Terminal ||
   4.184 -  at_mode -- antiq >> Antiquote) x
   4.185 -and body4e x = (Scan.option body4 >> (cat o the_list)) x;
   4.186 -
   4.187 -val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
   4.188 -val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
   4.189 -val rules = enum1 ";" (Scan.option rule) >> map_filter I;
   4.190 -
   4.191 -in
   4.192 -
   4.193 -val read =
   4.194 -  #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
   4.195 -
   4.196 -end;
   4.197 -
   4.198 -
   4.199 -(* latex output *)
   4.200 -
   4.201 -local
   4.202 -
   4.203 -fun vertical_range_cat (Cat (_, rails)) y =
   4.204 -  let val (rails', (_, y')) =
   4.205 -    fold_map (fn rail => fn (y0, y') =>
   4.206 -      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
   4.207 -      else
   4.208 -        let val (rail', y0') = vertical_range rail y0;
   4.209 -        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
   4.210 -  in (Cat (y, rails'), y') end
   4.211 -
   4.212 -and vertical_range (Bar cats) y =
   4.213 -      let val (cats', y') = fold_map vertical_range_cat cats y
   4.214 -      in (Bar cats', Int.max (y + 1, y')) end
   4.215 -  | vertical_range (Plus (cat1, cat2)) y =
   4.216 -      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
   4.217 -      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
   4.218 -  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   4.219 -  | vertical_range atom y = (atom, y + 1);
   4.220 -
   4.221 -fun output_rules state rules =
   4.222 -  let
   4.223 -    val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
   4.224 -    fun output_text b s =
   4.225 -      Output.output s
   4.226 -      |> b ? enclose "\\isakeyword{" "}"
   4.227 -      |> enclose "\\isa{" "}";
   4.228 -
   4.229 -    fun output_cat c (Cat (_, rails)) = outputs c rails
   4.230 -    and outputs c [rail] = output c rail
   4.231 -      | outputs _ rails = implode (map (output "") rails)
   4.232 -    and output _ (Bar []) = ""
   4.233 -      | output c (Bar [cat]) = output_cat c cat
   4.234 -      | output _ (Bar (cat :: cats)) =
   4.235 -          "\\rail@bar\n" ^ output_cat "" cat ^
   4.236 -          implode (map (fn Cat (y, rails) =>
   4.237 -              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
   4.238 -          "\\rail@endbar\n"
   4.239 -      | output c (Plus (cat, Cat (y, rails))) =
   4.240 -          "\\rail@plus\n" ^ output_cat c cat ^
   4.241 -          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
   4.242 -          "\\rail@endplus\n"
   4.243 -      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
   4.244 -      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
   4.245 -      | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
   4.246 -      | output c (Antiquote (b, a)) =
   4.247 -          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
   4.248 -
   4.249 -    fun output_rule (name, rail) =
   4.250 -      let
   4.251 -        val (rail', y') = vertical_range rail 0;
   4.252 -        val out_name =
   4.253 -          (case name of
   4.254 -            Antiquote.Text "" => ""
   4.255 -          | Antiquote.Text s => output_text false s
   4.256 -          | Antiquote.Antiq a => output_antiq a);
   4.257 -      in
   4.258 -        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
   4.259 -        output "" rail' ^
   4.260 -        "\\rail@end\n"
   4.261 -      end;
   4.262 -  in
   4.263 -    "\\begin{railoutput}\n" ^
   4.264 -    implode (map output_rule rules) ^
   4.265 -    "\\end{railoutput}\n"
   4.266 -  end;
   4.267 -
   4.268 -in
   4.269 -
   4.270 -val _ = Theory.setup
   4.271 -  (Thy_Output.antiquotation (Binding.name "rail")
   4.272 -    (Scan.lift (Parse.source_position Parse.string))
   4.273 -    (fn {state, ...} => output_rules state o read));
   4.274 -
   4.275 -end;
   4.276 -
   4.277 -end;
   4.278 -
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/Tools/rail.ML	Fri Jan 17 20:31:39 2014 +0100
     5.3 @@ -0,0 +1,275 @@
     5.4 +(*  Title:      Pure/Tools/rail.ML
     5.5 +    Author:     Michael Kerscher, TU München
     5.6 +    Author:     Makarius
     5.7 +
     5.8 +Railroad diagrams in LaTeX.
     5.9 +*)
    5.10 +
    5.11 +structure Rail: sig end =
    5.12 +struct
    5.13 +
    5.14 +(** lexical syntax **)
    5.15 +
    5.16 +(* datatype token *)
    5.17 +
    5.18 +datatype kind =
    5.19 +  Keyword | Ident | String | Antiq of Symbol_Pos.T list * Position.range | EOF;
    5.20 +
    5.21 +datatype token = Token of Position.range * (kind * string);
    5.22 +
    5.23 +fun pos_of (Token ((pos, _), _)) = pos;
    5.24 +fun end_pos_of (Token ((_, pos), _)) = pos;
    5.25 +
    5.26 +fun kind_of (Token (_, (k, _))) = k;
    5.27 +fun content_of (Token (_, (_, x))) = x;
    5.28 +
    5.29 +
    5.30 +(* diagnostics *)
    5.31 +
    5.32 +val print_kind =
    5.33 + fn Keyword => "rail keyword"
    5.34 +  | Ident => "identifier"
    5.35 +  | String => "single-quoted string"
    5.36 +  | Antiq _ => "antiquotation"
    5.37 +  | EOF => "end-of-input";
    5.38 +
    5.39 +fun print (Token ((pos, _), (k, x))) =
    5.40 +  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
    5.41 +  Position.here pos;
    5.42 +
    5.43 +fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
    5.44 +
    5.45 +
    5.46 +(* stopper *)
    5.47 +
    5.48 +fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
    5.49 +val eof = mk_eof Position.none;
    5.50 +
    5.51 +fun is_eof (Token (_, (EOF, _))) = true
    5.52 +  | is_eof _ = false;
    5.53 +
    5.54 +val stopper =
    5.55 +  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
    5.56 +
    5.57 +
    5.58 +(* tokenize *)
    5.59 +
    5.60 +local
    5.61 +
    5.62 +fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
    5.63 +
    5.64 +val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
    5.65 +
    5.66 +val scan_keyword =
    5.67 +  Scan.one
    5.68 +    (member (op =) ["|", "*", "+", "?", "(", ")", "\<newline>", ";", ":", "@"] o Symbol_Pos.symbol);
    5.69 +
    5.70 +val err_prefix = "Rail lexical error: ";
    5.71 +
    5.72 +val scan_token =
    5.73 +  scan_space >> K [] ||
    5.74 +  Antiquote.scan_antiq >> (fn antiq as (ss, _) => token (Antiq antiq) ss) ||
    5.75 +  scan_keyword >> (token Keyword o single) ||
    5.76 +  Lexicon.scan_id >> token Ident ||
    5.77 +  Symbol_Pos.scan_string_q err_prefix >> (token String o #1 o #2);
    5.78 +
    5.79 +val scan =
    5.80 +  (Scan.repeat scan_token >> flat) --|
    5.81 +    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
    5.82 +      (Scan.ahead (Scan.one Symbol_Pos.is_eof));
    5.83 +
    5.84 +in
    5.85 +
    5.86 +val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan) o Symbol_Pos.explode;
    5.87 +
    5.88 +end;
    5.89 +
    5.90 +
    5.91 +
    5.92 +(** parsing **)
    5.93 +
    5.94 +fun !!! scan =
    5.95 +  let
    5.96 +    val prefix = "Rail syntax error";
    5.97 +
    5.98 +    fun get_pos [] = " (end-of-input)"
    5.99 +      | get_pos (tok :: _) = Position.here (pos_of tok);
   5.100 +
   5.101 +    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
   5.102 +      | err (toks, SOME msg) =
   5.103 +          (fn () =>
   5.104 +            let val s = msg () in
   5.105 +              if String.isPrefix prefix s then s
   5.106 +              else prefix ^ get_pos toks ^ ": " ^ s
   5.107 +            end);
   5.108 +  in Scan.!! err scan end;
   5.109 +
   5.110 +fun $$$ x =
   5.111 +  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
   5.112 +  Scan.fail_with
   5.113 +    (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
   5.114 +      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
   5.115 +
   5.116 +fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
   5.117 +fun enum sep scan = enum1 sep scan || Scan.succeed [];
   5.118 +
   5.119 +val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
   5.120 +val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
   5.121 +
   5.122 +val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
   5.123 +
   5.124 +
   5.125 +
   5.126 +(** rail expressions **)
   5.127 +
   5.128 +(* datatype *)
   5.129 +
   5.130 +datatype rails =
   5.131 +  Cat of int * rail list
   5.132 +and rail =
   5.133 +  Bar of rails list |
   5.134 +  Plus of rails * rails |
   5.135 +  Newline of int |
   5.136 +  Nonterminal of string |
   5.137 +  Terminal of bool * string |
   5.138 +  Antiquote of bool * (Symbol_Pos.T list * Position.range);
   5.139 +
   5.140 +fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
   5.141 +and reverse (Bar cats) = Bar (map reverse_cat cats)
   5.142 +  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
   5.143 +  | reverse x = x;
   5.144 +
   5.145 +fun cat rails = Cat (0, rails);
   5.146 +
   5.147 +val empty = cat [];
   5.148 +fun is_empty (Cat (_, [])) = true | is_empty _ = false;
   5.149 +
   5.150 +fun is_newline (Newline _) = true | is_newline _ = false;
   5.151 +
   5.152 +fun bar [Cat (_, [rail])] = rail
   5.153 +  | bar cats = Bar cats;
   5.154 +
   5.155 +fun plus cat1 cat2 = Plus (cat1, reverse_cat cat2);
   5.156 +
   5.157 +fun star cat1 cat2 =
   5.158 +  if is_empty cat2 then plus empty cat1
   5.159 +  else bar [empty, cat [plus cat1 cat2]];
   5.160 +
   5.161 +fun maybe rail = bar [empty, cat [rail]];
   5.162 +
   5.163 +
   5.164 +(* read *)
   5.165 +
   5.166 +local
   5.167 +
   5.168 +val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
   5.169 +
   5.170 +fun body x = (enum1 "|" body1 >> bar) x
   5.171 +and body0 x = (enum "|" body1 >> bar) x
   5.172 +and body1 x =
   5.173 + (body2 :|-- (fn a =>
   5.174 +   $$$ "*" |-- !!! body4e >> (cat o single o star a) ||
   5.175 +   $$$ "+" |-- !!! body4e >> (cat o single o plus a) ||
   5.176 +   Scan.succeed a)) x
   5.177 +and body2 x = (Scan.repeat1 body3 >> cat) x
   5.178 +and body3 x = (body4 :|-- (fn a => $$$ "?" >> K (maybe a) || Scan.succeed a)) x
   5.179 +and body4 x =
   5.180 + ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
   5.181 +  $$$ "\<newline>" >> K (Newline 0) ||
   5.182 +  ident >> Nonterminal ||
   5.183 +  at_mode -- string >> Terminal ||
   5.184 +  at_mode -- antiq >> Antiquote) x
   5.185 +and body4e x = (Scan.option body4 >> (cat o the_list)) x;
   5.186 +
   5.187 +val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
   5.188 +val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
   5.189 +val rules = enum1 ";" (Scan.option rule) >> map_filter I;
   5.190 +
   5.191 +in
   5.192 +
   5.193 +val read =
   5.194 +  #1 o Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) o tokenize;
   5.195 +
   5.196 +end;
   5.197 +
   5.198 +
   5.199 +(* latex output *)
   5.200 +
   5.201 +local
   5.202 +
   5.203 +fun vertical_range_cat (Cat (_, rails)) y =
   5.204 +  let val (rails', (_, y')) =
   5.205 +    fold_map (fn rail => fn (y0, y') =>
   5.206 +      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
   5.207 +      else
   5.208 +        let val (rail', y0') = vertical_range rail y0;
   5.209 +        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
   5.210 +  in (Cat (y, rails'), y') end
   5.211 +
   5.212 +and vertical_range (Bar cats) y =
   5.213 +      let val (cats', y') = fold_map vertical_range_cat cats y
   5.214 +      in (Bar cats', Int.max (y + 1, y')) end
   5.215 +  | vertical_range (Plus (cat1, cat2)) y =
   5.216 +      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
   5.217 +      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
   5.218 +  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
   5.219 +  | vertical_range atom y = (atom, y + 1);
   5.220 +
   5.221 +fun output_rules state rules =
   5.222 +  let
   5.223 +    val output_antiq = Thy_Output.eval_antiq (#1 (Keyword.get_lexicons ())) state;
   5.224 +    fun output_text b s =
   5.225 +      Output.output s
   5.226 +      |> b ? enclose "\\isakeyword{" "}"
   5.227 +      |> enclose "\\isa{" "}";
   5.228 +
   5.229 +    fun output_cat c (Cat (_, rails)) = outputs c rails
   5.230 +    and outputs c [rail] = output c rail
   5.231 +      | outputs _ rails = implode (map (output "") rails)
   5.232 +    and output _ (Bar []) = ""
   5.233 +      | output c (Bar [cat]) = output_cat c cat
   5.234 +      | output _ (Bar (cat :: cats)) =
   5.235 +          "\\rail@bar\n" ^ output_cat "" cat ^
   5.236 +          implode (map (fn Cat (y, rails) =>
   5.237 +              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
   5.238 +          "\\rail@endbar\n"
   5.239 +      | output c (Plus (cat, Cat (y, rails))) =
   5.240 +          "\\rail@plus\n" ^ output_cat c cat ^
   5.241 +          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
   5.242 +          "\\rail@endplus\n"
   5.243 +      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
   5.244 +      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
   5.245 +      | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
   5.246 +      | output c (Antiquote (b, a)) =
   5.247 +          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
   5.248 +
   5.249 +    fun output_rule (name, rail) =
   5.250 +      let
   5.251 +        val (rail', y') = vertical_range rail 0;
   5.252 +        val out_name =
   5.253 +          (case name of
   5.254 +            Antiquote.Text "" => ""
   5.255 +          | Antiquote.Text s => output_text false s
   5.256 +          | Antiquote.Antiq a => output_antiq a);
   5.257 +      in
   5.258 +        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
   5.259 +        output "" rail' ^
   5.260 +        "\\rail@end\n"
   5.261 +      end;
   5.262 +  in
   5.263 +    "\\begin{railoutput}\n" ^
   5.264 +    implode (map output_rule rules) ^
   5.265 +    "\\end{railoutput}\n"
   5.266 +  end;
   5.267 +
   5.268 +in
   5.269 +
   5.270 +val _ = Theory.setup
   5.271 +  (Thy_Output.antiquotation @{binding rail}
   5.272 +    (Scan.lift (Parse.source_position Parse.string))
   5.273 +    (fn {state, ...} => output_rules state o read));
   5.274 +
   5.275 +end;
   5.276 +
   5.277 +end;
   5.278 +