src/Pure/Tools/rail.ML
author wenzelm
Fri Apr 01 21:34:17 2016 +0200 (2016-04-01)
changeset 62806 de9bf8171626
parent 62797 e08c44eed27f
child 67147 dea94b1aabc3
permissions -rw-r--r--
more markup;
wenzelm@55030
     1
(*  Title:      Pure/Tools/rail.ML
wenzelm@42504
     2
    Author:     Michael Kerscher, TU M√ľnchen
wenzelm@42504
     3
    Author:     Makarius
wenzelm@42504
     4
wenzelm@42504
     5
Railroad diagrams in LaTeX.
wenzelm@42504
     6
*)
wenzelm@42504
     7
wenzelm@62748
     8
signature RAIL =
wenzelm@62748
     9
sig
wenzelm@62748
    10
  datatype rails =
wenzelm@62748
    11
    Cat of int * rail list
wenzelm@62748
    12
  and rail =
wenzelm@62748
    13
    Bar of rails list |
wenzelm@62748
    14
    Plus of rails * rails |
wenzelm@62748
    15
    Newline of int |
wenzelm@62748
    16
    Nonterminal of string |
wenzelm@62748
    17
    Terminal of bool * string |
wenzelm@62748
    18
    Antiquote of bool * Antiquote.antiq
wenzelm@62748
    19
  val read: Proof.context -> Input.source -> (string Antiquote.antiquote * rail) list
wenzelm@62748
    20
  val output_rules: Toplevel.state -> (string Antiquote.antiquote * rail) list -> string
wenzelm@62748
    21
end;
wenzelm@62748
    22
wenzelm@62748
    23
structure Rail: RAIL =
wenzelm@42504
    24
struct
wenzelm@42504
    25
wenzelm@42504
    26
(** lexical syntax **)
wenzelm@42504
    27
wenzelm@56165
    28
(* singleton keywords *)
wenzelm@56165
    29
wenzelm@56165
    30
val keywords =
wenzelm@56165
    31
  Symtab.make [
wenzelm@56165
    32
    ("|", Markup.keyword3),
wenzelm@56165
    33
    ("*", Markup.keyword3),
wenzelm@56165
    34
    ("+", Markup.keyword3),
wenzelm@56165
    35
    ("?", Markup.keyword3),
wenzelm@56165
    36
    ("(", Markup.empty),
wenzelm@56165
    37
    (")", Markup.empty),
wenzelm@56165
    38
    ("\<newline>", Markup.keyword2),
wenzelm@56165
    39
    (";", Markup.keyword2),
wenzelm@56165
    40
    (":", Markup.keyword2),
wenzelm@56165
    41
    ("@", Markup.keyword1)];
wenzelm@56165
    42
wenzelm@56165
    43
wenzelm@42504
    44
(* datatype token *)
wenzelm@42504
    45
wenzelm@42508
    46
datatype kind =
wenzelm@55526
    47
  Keyword | Ident | String | Antiq of Antiquote.antiq | EOF;
wenzelm@42504
    48
wenzelm@42504
    49
datatype token = Token of Position.range * (kind * string);
wenzelm@42504
    50
wenzelm@42504
    51
fun pos_of (Token ((pos, _), _)) = pos;
wenzelm@42504
    52
fun end_pos_of (Token ((_, pos), _)) = pos;
wenzelm@42504
    53
wenzelm@58465
    54
fun range_of (toks as tok :: _) =
wenzelm@58465
    55
      let val pos' = end_pos_of (List.last toks)
wenzelm@62797
    56
      in Position.range (pos_of tok, pos') end
wenzelm@58465
    57
  | range_of [] = Position.no_range;
wenzelm@58465
    58
wenzelm@42504
    59
fun kind_of (Token (_, (k, _))) = k;
wenzelm@42504
    60
fun content_of (Token (_, (_, x))) = x;
wenzelm@42504
    61
wenzelm@42504
    62
wenzelm@42504
    63
(* diagnostics *)
wenzelm@42504
    64
wenzelm@42504
    65
val print_kind =
wenzelm@42504
    66
 fn Keyword => "rail keyword"
wenzelm@42504
    67
  | Ident => "identifier"
wenzelm@42504
    68
  | String => "single-quoted string"
wenzelm@42508
    69
  | Antiq _ => "antiquotation"
wenzelm@48911
    70
  | EOF => "end-of-input";
wenzelm@42504
    71
wenzelm@42504
    72
fun print (Token ((pos, _), (k, x))) =
wenzelm@42504
    73
  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
wenzelm@48992
    74
  Position.here pos;
wenzelm@42504
    75
wenzelm@42504
    76
fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
wenzelm@42504
    77
wenzelm@55613
    78
fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
wenzelm@56163
    79
  | reports_of_token (Token ((pos, _), (Keyword, x))) =
wenzelm@56165
    80
      map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
wenzelm@61457
    81
  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports [Antiquote.Antiq antiq]
wenzelm@55613
    82
  | reports_of_token _ = [];
wenzelm@55613
    83
wenzelm@42504
    84
wenzelm@42504
    85
(* stopper *)
wenzelm@42504
    86
wenzelm@42504
    87
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
wenzelm@42504
    88
val eof = mk_eof Position.none;
wenzelm@42504
    89
wenzelm@42504
    90
fun is_eof (Token (_, (EOF, _))) = true
wenzelm@42504
    91
  | is_eof _ = false;
wenzelm@42504
    92
wenzelm@42504
    93
val stopper =
wenzelm@42504
    94
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
wenzelm@42504
    95
wenzelm@42504
    96
wenzelm@42504
    97
(* tokenize *)
wenzelm@42504
    98
wenzelm@42504
    99
local
wenzelm@42504
   100
wenzelm@42504
   101
fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
wenzelm@42504
   102
wenzelm@61473
   103
fun antiq_token antiq =
wenzelm@61473
   104
  [Token (#range antiq, (Antiq antiq, Symbol_Pos.content (#body antiq)))];
wenzelm@58465
   105
wenzelm@42504
   106
val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
wenzelm@42504
   107
wenzelm@42504
   108
val scan_keyword =
wenzelm@56165
   109
  Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
wenzelm@42504
   110
wenzelm@48764
   111
val err_prefix = "Rail lexical error: ";
wenzelm@48764
   112
wenzelm@42504
   113
val scan_token =
wenzelm@42504
   114
  scan_space >> K [] ||
wenzelm@58465
   115
  Antiquote.scan_antiq >> antiq_token ||
wenzelm@42504
   116
  scan_keyword >> (token Keyword o single) ||
wenzelm@42504
   117
  Lexicon.scan_id >> token Ident ||
wenzelm@55613
   118
  Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
wenzelm@62797
   119
    [Token (Position.range (pos1, pos2), (String, Symbol_Pos.content ss))]);
wenzelm@42504
   120
wenzelm@42506
   121
val scan =
wenzelm@61476
   122
  Scan.repeats scan_token --|
wenzelm@48764
   123
    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
wenzelm@42506
   124
      (Scan.ahead (Scan.one Symbol_Pos.is_eof));
wenzelm@42506
   125
wenzelm@42504
   126
in
wenzelm@42504
   127
wenzelm@55613
   128
val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
wenzelm@42504
   129
wenzelm@42504
   130
end;
wenzelm@42504
   131
wenzelm@42504
   132
wenzelm@42504
   133
wenzelm@42504
   134
(** parsing **)
wenzelm@42504
   135
wenzelm@58465
   136
(* parser combinators *)
wenzelm@58465
   137
wenzelm@42504
   138
fun !!! scan =
wenzelm@42504
   139
  let
wenzelm@42504
   140
    val prefix = "Rail syntax error";
wenzelm@42504
   141
wenzelm@48911
   142
    fun get_pos [] = " (end-of-input)"
wenzelm@48992
   143
      | get_pos (tok :: _) = Position.here (pos_of tok);
wenzelm@42504
   144
wenzelm@43947
   145
    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
wenzelm@42504
   146
      | err (toks, SOME msg) =
wenzelm@43947
   147
          (fn () =>
wenzelm@43947
   148
            let val s = msg () in
wenzelm@43947
   149
              if String.isPrefix prefix s then s
wenzelm@43947
   150
              else prefix ^ get_pos toks ^ ": " ^ s
wenzelm@43947
   151
            end);
wenzelm@42504
   152
  in Scan.!! err scan end;
wenzelm@42504
   153
wenzelm@42504
   154
fun $$$ x =
wenzelm@42504
   155
  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
wenzelm@42504
   156
  Scan.fail_with
wenzelm@48911
   157
    (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
wenzelm@43947
   158
      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
wenzelm@42504
   159
wenzelm@42504
   160
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
wenzelm@42504
   161
fun enum sep scan = enum1 sep scan || Scan.succeed [];
wenzelm@42504
   162
wenzelm@42508
   163
val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
wenzelm@42508
   164
val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
wenzelm@42504
   165
wenzelm@42508
   166
val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
wenzelm@42504
   167
wenzelm@58465
   168
fun RANGE scan = Scan.trace scan >> apsnd range_of;
wenzelm@58465
   169
fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
wenzelm@58465
   170
wenzelm@58465
   171
wenzelm@58465
   172
(* parse trees *)
wenzelm@58465
   173
wenzelm@58465
   174
datatype trees =
wenzelm@58465
   175
  CAT of tree list * Position.range
wenzelm@58465
   176
and tree =
wenzelm@58465
   177
  BAR of trees list * Position.range |
wenzelm@58465
   178
  STAR of (trees * trees) * Position.range |
wenzelm@58465
   179
  PLUS of (trees * trees) * Position.range |
wenzelm@58465
   180
  MAYBE of tree * Position.range |
wenzelm@58465
   181
  NEWLINE of Position.range |
wenzelm@58465
   182
  NONTERMINAL of string * Position.range |
wenzelm@58465
   183
  TERMINAL of (bool * string) * Position.range |
wenzelm@58465
   184
  ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
wenzelm@58465
   185
wenzelm@58465
   186
fun reports_of_tree ctxt =
wenzelm@58465
   187
  if Context_Position.is_visible ctxt then
wenzelm@58465
   188
    let
wenzelm@58465
   189
      fun reports r =
wenzelm@58465
   190
        if r = Position.no_range then []
wenzelm@62806
   191
        else [(Position.range_position r, Markup.expression "")];
wenzelm@58465
   192
      fun trees (CAT (ts, r)) = reports r @ maps tree ts
wenzelm@58465
   193
      and tree (BAR (Ts, r)) = reports r @ maps trees Ts
wenzelm@58465
   194
        | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
wenzelm@58465
   195
        | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
wenzelm@58465
   196
        | tree (MAYBE (t, r)) = reports r @ tree t
wenzelm@58465
   197
        | tree (NEWLINE r) = reports r
wenzelm@58465
   198
        | tree (NONTERMINAL (_, r)) = reports r
wenzelm@58465
   199
        | tree (TERMINAL (_, r)) = reports r
wenzelm@58465
   200
        | tree (ANTIQUOTE (_, r)) = reports r;
wenzelm@58465
   201
    in distinct (op =) o tree end
wenzelm@58465
   202
  else K [];
wenzelm@58465
   203
wenzelm@58465
   204
local
wenzelm@58465
   205
wenzelm@58465
   206
val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
wenzelm@58465
   207
wenzelm@58465
   208
fun body x = (RANGE (enum1 "|" body1) >> BAR) x
wenzelm@58465
   209
and body0 x = (RANGE (enum "|" body1) >> BAR) x
wenzelm@58465
   210
and body1 x =
wenzelm@58465
   211
 (RANGE_APP (body2 :|-- (fn a =>
wenzelm@58465
   212
   $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
wenzelm@58465
   213
   $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
wenzelm@58465
   214
   Scan.succeed (K a)))) x
wenzelm@58465
   215
and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
wenzelm@58465
   216
and body3 x =
wenzelm@58465
   217
 (RANGE_APP (body4 :|-- (fn a =>
wenzelm@58465
   218
   $$$ "?" >> K (curry MAYBE a) ||
wenzelm@58465
   219
   Scan.succeed (K a)))) x
wenzelm@58465
   220
and body4 x =
wenzelm@58465
   221
 ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
wenzelm@58465
   222
  RANGE_APP
wenzelm@58465
   223
   ($$$ "\<newline>" >> K NEWLINE ||
wenzelm@58465
   224
    ident >> curry NONTERMINAL ||
wenzelm@58465
   225
    at_mode -- string >> curry TERMINAL ||
wenzelm@58465
   226
    at_mode -- antiq >> curry ANTIQUOTE)) x
wenzelm@58465
   227
and body4e x =
wenzelm@58465
   228
  (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
wenzelm@58465
   229
wenzelm@58465
   230
val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
wenzelm@58465
   231
val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
wenzelm@58465
   232
val rules = enum1 ";" (Scan.option rule) >> map_filter I;
wenzelm@58465
   233
wenzelm@58465
   234
in
wenzelm@58465
   235
wenzelm@58465
   236
fun parse_rules toks =
wenzelm@58465
   237
  #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
wenzelm@58465
   238
wenzelm@58465
   239
end;
wenzelm@42504
   240
wenzelm@42504
   241
wenzelm@42504
   242
(** rail expressions **)
wenzelm@42504
   243
wenzelm@42504
   244
(* datatype *)
wenzelm@42504
   245
wenzelm@42504
   246
datatype rails =
wenzelm@42504
   247
  Cat of int * rail list
wenzelm@42504
   248
and rail =
wenzelm@42504
   249
  Bar of rails list |
wenzelm@42504
   250
  Plus of rails * rails |
wenzelm@42504
   251
  Newline of int |
wenzelm@42504
   252
  Nonterminal of string |
wenzelm@42516
   253
  Terminal of bool * string |
wenzelm@55526
   254
  Antiquote of bool * Antiquote.antiq;
wenzelm@42504
   255
wenzelm@58465
   256
fun is_newline (Newline _) = true | is_newline _ = false;
wenzelm@58465
   257
wenzelm@58465
   258
wenzelm@58465
   259
(* prepare *)
wenzelm@58465
   260
wenzelm@58465
   261
local
wenzelm@42504
   262
wenzelm@42504
   263
fun cat rails = Cat (0, rails);
wenzelm@42504
   264
wenzelm@42504
   265
val empty = cat [];
wenzelm@42504
   266
fun is_empty (Cat (_, [])) = true | is_empty _ = false;
wenzelm@42504
   267
wenzelm@42504
   268
fun bar [Cat (_, [rail])] = rail
wenzelm@42504
   269
  | bar cats = Bar cats;
wenzelm@42504
   270
wenzelm@58465
   271
fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
wenzelm@58465
   272
and reverse (Bar cats) = Bar (map reverse_cat cats)
wenzelm@58465
   273
  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
wenzelm@58465
   274
  | reverse x = x;
wenzelm@58465
   275
wenzelm@58465
   276
fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
wenzelm@58465
   277
wenzelm@58465
   278
in
wenzelm@42504
   279
wenzelm@58465
   280
fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
wenzelm@58465
   281
and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
wenzelm@58465
   282
  | prepare_tree (STAR (Ts, _)) =
wenzelm@59058
   283
      let val (cat1, cat2) = apply2 prepare_trees Ts in
wenzelm@58465
   284
        if is_empty cat2 then plus (empty, cat1)
wenzelm@58465
   285
        else bar [empty, cat [plus (cat1, cat2)]]
wenzelm@58465
   286
      end
wenzelm@59058
   287
  | prepare_tree (PLUS (Ts, _)) = plus (apply2 prepare_trees Ts)
wenzelm@58465
   288
  | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
wenzelm@58465
   289
  | prepare_tree (NEWLINE _) = Newline 0
wenzelm@58465
   290
  | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
wenzelm@58465
   291
  | prepare_tree (TERMINAL (a, _)) = Terminal a
wenzelm@58465
   292
  | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
wenzelm@42504
   293
wenzelm@58465
   294
end;
wenzelm@42504
   295
wenzelm@42504
   296
wenzelm@42504
   297
(* read *)
wenzelm@42504
   298
wenzelm@59064
   299
fun read ctxt source =
wenzelm@55613
   300
  let
wenzelm@59064
   301
    val _ = Context_Position.report ctxt (Input.pos_of source) Markup.language_rail;
wenzelm@59064
   302
    val toks = tokenize (Input.source_explode source);
wenzelm@55613
   303
    val _ = Context_Position.reports ctxt (maps reports_of_token toks);
wenzelm@58465
   304
    val rules = parse_rules toks;
wenzelm@58465
   305
    val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);
wenzelm@58465
   306
  in map (apsnd prepare_tree) rules end;
wenzelm@42504
   307
wenzelm@42504
   308
wenzelm@42504
   309
(* latex output *)
wenzelm@42504
   310
wenzelm@42504
   311
local
wenzelm@42504
   312
wenzelm@42504
   313
fun vertical_range_cat (Cat (_, rails)) y =
wenzelm@42504
   314
  let val (rails', (_, y')) =
wenzelm@42504
   315
    fold_map (fn rail => fn (y0, y') =>
wenzelm@42504
   316
      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
wenzelm@42504
   317
      else
wenzelm@42504
   318
        let val (rail', y0') = vertical_range rail y0;
wenzelm@42504
   319
        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
wenzelm@42504
   320
  in (Cat (y, rails'), y') end
wenzelm@42504
   321
wenzelm@42504
   322
and vertical_range (Bar cats) y =
wenzelm@42504
   323
      let val (cats', y') = fold_map vertical_range_cat cats y
wenzelm@42504
   324
      in (Bar cats', Int.max (y + 1, y')) end
wenzelm@42504
   325
  | vertical_range (Plus (cat1, cat2)) y =
wenzelm@42504
   326
      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
wenzelm@42504
   327
      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
wenzelm@42504
   328
  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
wenzelm@42504
   329
  | vertical_range atom y = (atom, y + 1);
wenzelm@42504
   330
wenzelm@62748
   331
in
wenzelm@62748
   332
wenzelm@42508
   333
fun output_rules state rules =
wenzelm@42508
   334
  let
wenzelm@61456
   335
    val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
wenzelm@42516
   336
    fun output_text b s =
wenzelm@42516
   337
      Output.output s
wenzelm@42516
   338
      |> b ? enclose "\\isakeyword{" "}"
wenzelm@42516
   339
      |> enclose "\\isa{" "}";
wenzelm@42504
   340
wenzelm@42508
   341
    fun output_cat c (Cat (_, rails)) = outputs c rails
wenzelm@42508
   342
    and outputs c [rail] = output c rail
wenzelm@42508
   343
      | outputs _ rails = implode (map (output "") rails)
wenzelm@42508
   344
    and output _ (Bar []) = ""
wenzelm@42508
   345
      | output c (Bar [cat]) = output_cat c cat
wenzelm@42508
   346
      | output _ (Bar (cat :: cats)) =
wenzelm@42508
   347
          "\\rail@bar\n" ^ output_cat "" cat ^
wenzelm@42508
   348
          implode (map (fn Cat (y, rails) =>
wenzelm@42508
   349
              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
wenzelm@42508
   350
          "\\rail@endbar\n"
wenzelm@42508
   351
      | output c (Plus (cat, Cat (y, rails))) =
wenzelm@42508
   352
          "\\rail@plus\n" ^ output_cat c cat ^
wenzelm@42508
   353
          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
wenzelm@42508
   354
          "\\rail@endplus\n"
wenzelm@42508
   355
      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
wenzelm@42516
   356
      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
wenzelm@42516
   357
      | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
wenzelm@42508
   358
      | output c (Antiquote (b, a)) =
wenzelm@42508
   359
          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
wenzelm@42504
   360
wenzelm@42508
   361
    fun output_rule (name, rail) =
wenzelm@42508
   362
      let
wenzelm@42508
   363
        val (rail', y') = vertical_range rail 0;
wenzelm@42508
   364
        val out_name =
wenzelm@42508
   365
          (case name of
wenzelm@42661
   366
            Antiquote.Text "" => ""
wenzelm@42661
   367
          | Antiquote.Text s => output_text false s
wenzelm@42508
   368
          | Antiquote.Antiq a => output_antiq a);
wenzelm@42508
   369
      in
wenzelm@42508
   370
        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
wenzelm@42508
   371
        output "" rail' ^
wenzelm@42508
   372
        "\\rail@end\n"
wenzelm@42508
   373
      end;
wenzelm@61462
   374
  in Latex.environment "railoutput" (implode (map output_rule rules)) end;
wenzelm@42504
   375
wenzelm@53171
   376
val _ = Theory.setup
wenzelm@59937
   377
  (Thy_Output.antiquotation @{binding rail} (Scan.lift Args.text_input)
wenzelm@55613
   378
    (fn {state, context, ...} => output_rules state o read context));
wenzelm@42504
   379
wenzelm@42504
   380
end;
wenzelm@42504
   381
wenzelm@42504
   382
end;