src/Pure/Tools/rail.ML
author wenzelm
Tue, 11 Nov 2014 18:16:25 +0100
changeset 58978 e42da880c61e
parent 58928 23d0ffd48006
child 59058 a78612c67ec0
permissions -rw-r--r--
more position information, e.g. relevant for errors in generated ML source;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55030
9a9049d12e21 prefer user-space tool within Pure.thy;
wenzelm
parents: 55029
diff changeset
     1
(*  Title:      Pure/Tools/rail.ML
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     2
    Author:     Michael Kerscher, TU M√ľnchen
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     4
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     5
Railroad diagrams in LaTeX.
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     6
*)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     7
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     8
structure Rail: sig end =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
     9
struct
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    10
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    11
(** lexical syntax **)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    12
56165
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    13
(* singleton keywords *)
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    14
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    15
val keywords =
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    16
  Symtab.make [
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    17
    ("|", Markup.keyword3),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    18
    ("*", Markup.keyword3),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    19
    ("+", Markup.keyword3),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    20
    ("?", Markup.keyword3),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    21
    ("(", Markup.empty),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    22
    (")", Markup.empty),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    23
    ("\<newline>", Markup.keyword2),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    24
    (";", Markup.keyword2),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    25
    (":", Markup.keyword2),
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    26
    ("@", Markup.keyword1)];
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    27
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    28
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    29
(* datatype token *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    30
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
    31
datatype kind =
55526
39708e59f4b0 more markup;
wenzelm
parents: 55112
diff changeset
    32
  Keyword | Ident | String | Antiq of Antiquote.antiq | EOF;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    33
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    34
datatype token = Token of Position.range * (kind * string);
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    35
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    36
fun pos_of (Token ((pos, _), _)) = pos;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    37
fun end_pos_of (Token ((_, pos), _)) = pos;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    38
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    39
fun range_of (toks as tok :: _) =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    40
      let val pos' = end_pos_of (List.last toks)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    41
      in Position.range (pos_of tok) pos' end
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    42
  | range_of [] = Position.no_range;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    43
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    44
fun kind_of (Token (_, (k, _))) = k;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    45
fun content_of (Token (_, (_, x))) = x;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    46
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    47
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    48
(* diagnostics *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    49
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    50
val print_kind =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    51
 fn Keyword => "rail keyword"
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    52
  | Ident => "identifier"
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    53
  | String => "single-quoted string"
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
    54
  | Antiq _ => "antiquotation"
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48764
diff changeset
    55
  | EOF => "end-of-input";
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    56
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    57
fun print (Token ((pos, _), (k, x))) =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    58
  (if k = EOF then print_kind k else print_kind k ^ " " ^ quote x) ^
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48911
diff changeset
    59
  Position.here pos;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    60
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    61
fun print_keyword x = print_kind Keyword ^ " " ^ quote x;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    62
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
    63
fun reports_of_token (Token ((pos, _), (String, _))) = [(pos, Markup.inner_string)]
56163
331f4aba14b3 more markup;
wenzelm
parents: 55828
diff changeset
    64
  | reports_of_token (Token ((pos, _), (Keyword, x))) =
56165
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    65
      map (pair pos) (the_list (Symtab.lookup keywords x) @ Completion.suppress_abbrevs x)
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
    66
  | reports_of_token (Token (_, (Antiq antiq, _))) = Antiquote.antiq_reports antiq
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
    67
  | reports_of_token _ = [];
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
    68
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    69
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    70
(* stopper *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    71
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    72
fun mk_eof pos = Token ((pos, Position.none), (EOF, ""));
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    73
val eof = mk_eof Position.none;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    74
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    75
fun is_eof (Token (_, (EOF, _))) = true
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    76
  | is_eof _ = false;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    77
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    78
val stopper =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    79
  Scan.stopper (fn [] => eof | toks => mk_eof (end_pos_of (List.last toks))) is_eof;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    80
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    81
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    82
(* tokenize *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    83
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    84
local
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    85
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    86
fun token k ss = [Token (Symbol_Pos.range ss, (k, Symbol_Pos.content ss))];
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    87
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    88
fun antiq_token (antiq as (ss, {range, ...})) =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    89
  [Token (range, (Antiq antiq, Symbol_Pos.content ss))];
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
    90
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    91
val scan_space = Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol);
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    92
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    93
val scan_keyword =
56165
dd89ce51d2c8 tuned markup;
wenzelm
parents: 56163
diff changeset
    94
  Scan.one (Symtab.defined keywords o Symbol_Pos.symbol);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    95
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 43947
diff changeset
    96
val err_prefix = "Rail lexical error: ";
4fe0920d5049 proper error prefixes;
wenzelm
parents: 43947
diff changeset
    97
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    98
val scan_token =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
    99
  scan_space >> K [] ||
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   100
  Antiquote.scan_antiq >> antiq_token ||
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   101
  scan_keyword >> (token Keyword o single) ||
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   102
  Lexicon.scan_id >> token Ident ||
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   103
  Symbol_Pos.scan_string_q err_prefix >> (fn (pos1, (ss, pos2)) =>
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   104
    [Token (Position.range pos1 pos2, (String, Symbol_Pos.content ss))]);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   105
42506
876887b07e8d more robust error handling (NB: Source.source requires total scanner or recover);
wenzelm
parents: 42504
diff changeset
   106
val scan =
876887b07e8d more robust error handling (NB: Source.source requires total scanner or recover);
wenzelm
parents: 42504
diff changeset
   107
  (Scan.repeat scan_token >> flat) --|
48764
4fe0920d5049 proper error prefixes;
wenzelm
parents: 43947
diff changeset
   108
    Symbol_Pos.!!! (fn () => err_prefix ^ "bad input")
42506
876887b07e8d more robust error handling (NB: Source.source requires total scanner or recover);
wenzelm
parents: 42504
diff changeset
   109
      (Scan.ahead (Scan.one Symbol_Pos.is_eof));
876887b07e8d more robust error handling (NB: Source.source requires total scanner or recover);
wenzelm
parents: 42504
diff changeset
   110
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   111
in
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   112
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   113
val tokenize = #1 o Scan.error (Scan.finite Symbol_Pos.stopper scan);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   114
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   115
end;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   116
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   117
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   118
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   119
(** parsing **)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   120
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   121
(* parser combinators *)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   122
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   123
fun !!! scan =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   124
  let
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   125
    val prefix = "Rail syntax error";
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   126
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48764
diff changeset
   127
    fun get_pos [] = " (end-of-input)"
48992
0518bf89c777 renamed Position.str_of to Position.here;
wenzelm
parents: 48911
diff changeset
   128
      | get_pos (tok :: _) = Position.here (pos_of tok);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   129
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   130
    fun err (toks, NONE) = (fn () => prefix ^ get_pos toks)
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   131
      | err (toks, SOME msg) =
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   132
          (fn () =>
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   133
            let val s = msg () in
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   134
              if String.isPrefix prefix s then s
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   135
              else prefix ^ get_pos toks ^ ": " ^ s
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   136
            end);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   137
  in Scan.!! err scan end;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   138
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   139
fun $$$ x =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   140
  Scan.one (fn tok => kind_of tok = Keyword andalso content_of tok = x) ||
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   141
  Scan.fail_with
48911
5debc3e4fa81 tuned messages: end-of-input rarely means physical end-of-file from the past;
wenzelm
parents: 48764
diff changeset
   142
    (fn [] => (fn () => print_keyword x ^ " expected,\nbut end-of-input was found")
43947
9b00f09f7721 defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents: 43564
diff changeset
   143
      | tok :: _ => (fn () => print_keyword x ^ " expected,\nbut " ^ print tok ^ " was found"));
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   144
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   145
fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   146
fun enum sep scan = enum1 sep scan || Scan.succeed [];
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   147
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   148
val ident = Scan.some (fn tok => if kind_of tok = Ident then SOME (content_of tok) else NONE);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   149
val string = Scan.some (fn tok => if kind_of tok = String then SOME (content_of tok) else NONE);
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   150
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   151
val antiq = Scan.some (fn tok => (case kind_of tok of Antiq a => SOME a | _ => NONE));
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   152
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   153
fun RANGE scan = Scan.trace scan >> apsnd range_of;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   154
fun RANGE_APP scan = RANGE scan >> (fn (f, r) => f r);
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   155
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   156
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   157
(* parse trees *)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   158
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   159
datatype trees =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   160
  CAT of tree list * Position.range
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   161
and tree =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   162
  BAR of trees list * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   163
  STAR of (trees * trees) * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   164
  PLUS of (trees * trees) * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   165
  MAYBE of tree * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   166
  NEWLINE of Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   167
  NONTERMINAL of string * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   168
  TERMINAL of (bool * string) * Position.range |
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   169
  ANTIQUOTE of (bool * Antiquote.antiq) * Position.range;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   170
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   171
fun reports_of_tree ctxt =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   172
  if Context_Position.is_visible ctxt then
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   173
    let
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   174
      fun reports r =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   175
        if r = Position.no_range then []
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   176
        else [(Position.set_range r, Markup.expression)];
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   177
      fun trees (CAT (ts, r)) = reports r @ maps tree ts
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   178
      and tree (BAR (Ts, r)) = reports r @ maps trees Ts
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   179
        | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   180
        | tree (PLUS ((T1, T2), r)) = reports r @ trees T1 @ trees T2
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   181
        | tree (MAYBE (t, r)) = reports r @ tree t
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   182
        | tree (NEWLINE r) = reports r
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   183
        | tree (NONTERMINAL (_, r)) = reports r
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   184
        | tree (TERMINAL (_, r)) = reports r
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   185
        | tree (ANTIQUOTE (_, r)) = reports r;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   186
    in distinct (op =) o tree end
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   187
  else K [];
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   188
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   189
local
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   190
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   191
val at_mode = Scan.option ($$$ "@") >> (fn NONE => false | _ => true);
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   192
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   193
fun body x = (RANGE (enum1 "|" body1) >> BAR) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   194
and body0 x = (RANGE (enum "|" body1) >> BAR) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   195
and body1 x =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   196
 (RANGE_APP (body2 :|-- (fn a =>
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   197
   $$$ "*" |-- !!! body4e >> (fn b => fn r => CAT ([STAR ((a, b), r)], r)) ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   198
   $$$ "+" |-- !!! body4e >> (fn b => fn r => CAT ([PLUS ((a, b), r)], r)) ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   199
   Scan.succeed (K a)))) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   200
and body2 x = (RANGE (Scan.repeat1 body3) >> CAT) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   201
and body3 x =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   202
 (RANGE_APP (body4 :|-- (fn a =>
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   203
   $$$ "?" >> K (curry MAYBE a) ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   204
   Scan.succeed (K a)))) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   205
and body4 x =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   206
 ($$$ "(" |-- !!! (body0 --| $$$ ")") ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   207
  RANGE_APP
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   208
   ($$$ "\<newline>" >> K NEWLINE ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   209
    ident >> curry NONTERMINAL ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   210
    at_mode -- string >> curry TERMINAL ||
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   211
    at_mode -- antiq >> curry ANTIQUOTE)) x
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   212
and body4e x =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   213
  (RANGE (Scan.option body4) >> (fn (a, r) => CAT (the_list a, r))) x;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   214
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   215
val rule_name = ident >> Antiquote.Text || antiq >> Antiquote.Antiq;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   216
val rule = rule_name -- ($$$ ":" |-- !!! body) || body >> pair (Antiquote.Text "");
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   217
val rules = enum1 ";" (Scan.option rule) >> map_filter I;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   218
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   219
in
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   220
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   221
fun parse_rules toks =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   222
  #1 (Scan.error (Scan.finite stopper (rules --| !!! (Scan.ahead (Scan.one is_eof)))) toks);
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   223
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   224
end;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   225
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   226
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   227
(** rail expressions **)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   228
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   229
(* datatype *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   230
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   231
datatype rails =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   232
  Cat of int * rail list
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   233
and rail =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   234
  Bar of rails list |
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   235
  Plus of rails * rails |
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   236
  Newline of int |
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   237
  Nonterminal of string |
42516
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   238
  Terminal of bool * string |
55526
39708e59f4b0 more markup;
wenzelm
parents: 55112
diff changeset
   239
  Antiquote of bool * Antiquote.antiq;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   240
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   241
fun is_newline (Newline _) = true | is_newline _ = false;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   242
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   243
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   244
(* prepare *)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   245
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   246
local
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   247
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   248
fun cat rails = Cat (0, rails);
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   249
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   250
val empty = cat [];
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   251
fun is_empty (Cat (_, [])) = true | is_empty _ = false;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   252
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   253
fun bar [Cat (_, [rail])] = rail
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   254
  | bar cats = Bar cats;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   255
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   256
fun reverse_cat (Cat (y, rails)) = Cat (y, rev (map reverse rails))
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   257
and reverse (Bar cats) = Bar (map reverse_cat cats)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   258
  | reverse (Plus (cat1, cat2)) = Plus (reverse_cat cat1, reverse_cat cat2)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   259
  | reverse x = x;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   260
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   261
fun plus (cat1, cat2) = Plus (cat1, reverse_cat cat2);
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   262
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   263
in
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   264
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   265
fun prepare_trees (CAT (ts, _)) = Cat (0, map prepare_tree ts)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   266
and prepare_tree (BAR (Ts, _)) = bar (map prepare_trees Ts)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   267
  | prepare_tree (STAR (Ts, _)) =
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   268
      let val (cat1, cat2) = pairself prepare_trees Ts in
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   269
        if is_empty cat2 then plus (empty, cat1)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   270
        else bar [empty, cat [plus (cat1, cat2)]]
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   271
      end
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   272
  | prepare_tree (PLUS (Ts, _)) = plus (pairself prepare_trees Ts)
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   273
  | prepare_tree (MAYBE (t, _)) = bar [empty, cat [prepare_tree t]]
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   274
  | prepare_tree (NEWLINE _) = Newline 0
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   275
  | prepare_tree (NONTERMINAL (a, _)) = Nonterminal a
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   276
  | prepare_tree (TERMINAL (a, _)) = Terminal a
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   277
  | prepare_tree (ANTIQUOTE (a, _)) = Antiquote a;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   278
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   279
end;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   280
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   281
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   282
(* read *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   283
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55613
diff changeset
   284
fun read ctxt (source: Symbol_Pos.source) =
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   285
  let
58978
e42da880c61e more position information, e.g. relevant for errors in generated ML source;
wenzelm
parents: 58928
diff changeset
   286
    val {text, range = (pos, _), ...} = source;
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   287
    val _ = Context_Position.report ctxt pos Markup.language_rail;
55828
42ac3cfb89f6 clarified language markup: added "delimited" property;
wenzelm
parents: 55613
diff changeset
   288
    val toks = tokenize (Symbol_Pos.explode (text, pos));
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   289
    val _ = Context_Position.reports ctxt (maps reports_of_token toks);
58465
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   290
    val rules = parse_rules toks;
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   291
    val _ = Position.reports (maps (reports_of_tree ctxt o #2) rules);
bd06c6479748 proper range for Antiq tokens;
wenzelm
parents: 56165
diff changeset
   292
  in map (apsnd prepare_tree) rules end;
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   293
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   294
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   295
(* latex output *)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   296
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   297
local
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   298
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   299
fun vertical_range_cat (Cat (_, rails)) y =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   300
  let val (rails', (_, y')) =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   301
    fold_map (fn rail => fn (y0, y') =>
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   302
      if is_newline rail then (Newline (y' + 1), (y' + 1, y' + 2))
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   303
      else
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   304
        let val (rail', y0') = vertical_range rail y0;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   305
        in (rail', (y0, Int.max (y0', y'))) end) rails (y, y + 1)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   306
  in (Cat (y, rails'), y') end
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   307
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   308
and vertical_range (Bar cats) y =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   309
      let val (cats', y') = fold_map vertical_range_cat cats y
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   310
      in (Bar cats', Int.max (y + 1, y')) end
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   311
  | vertical_range (Plus (cat1, cat2)) y =
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   312
      let val ([cat1', cat2'], y') = fold_map vertical_range_cat [cat1, cat2] y;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   313
      in (Plus (cat1', cat2'), Int.max (y + 1, y')) end
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   314
  | vertical_range (Newline _) y = (Newline (y + 2), y + 3)
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   315
  | vertical_range atom y = (atom, y + 1);
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   316
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   317
fun output_rules state rules =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   318
  let
58928
23d0ffd48006 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents: 58903
diff changeset
   319
    val output_antiq = Thy_Output.eval_antiq state;
42516
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   320
    fun output_text b s =
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   321
      Output.output s
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   322
      |> b ? enclose "\\isakeyword{" "}"
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   323
      |> enclose "\\isa{" "}";
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   324
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   325
    fun output_cat c (Cat (_, rails)) = outputs c rails
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   326
    and outputs c [rail] = output c rail
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   327
      | outputs _ rails = implode (map (output "") rails)
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   328
    and output _ (Bar []) = ""
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   329
      | output c (Bar [cat]) = output_cat c cat
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   330
      | output _ (Bar (cat :: cats)) =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   331
          "\\rail@bar\n" ^ output_cat "" cat ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   332
          implode (map (fn Cat (y, rails) =>
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   333
              "\\rail@nextbar{" ^ string_of_int y ^ "}\n" ^ outputs "" rails) cats) ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   334
          "\\rail@endbar\n"
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   335
      | output c (Plus (cat, Cat (y, rails))) =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   336
          "\\rail@plus\n" ^ output_cat c cat ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   337
          "\\rail@nextplus{" ^ string_of_int y ^ "}\n" ^ outputs "c" rails ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   338
          "\\rail@endplus\n"
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   339
      | output _ (Newline y) = "\\rail@cr{" ^ string_of_int y ^ "}\n"
42516
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   340
      | output c (Nonterminal s) = "\\rail@" ^ c ^ "nont{" ^ output_text false s ^ "}[]\n"
11417d1eff3b treat @ as separate keyword;
wenzelm
parents: 42508
diff changeset
   341
      | output c (Terminal (b, s)) = "\\rail@" ^ c ^ "term{" ^ output_text b s ^ "}[]\n"
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   342
      | output c (Antiquote (b, a)) =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   343
          "\\rail@" ^ c ^ (if b then "term{" else "nont{") ^ output_antiq a ^ "}[]\n";
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   344
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   345
    fun output_rule (name, rail) =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   346
      let
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   347
        val (rail', y') = vertical_range rail 0;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   348
        val out_name =
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   349
          (case name of
42661
824d3f1d8de6 proper treatment of empty name -- avoid excessive vertical space;
wenzelm
parents: 42657
diff changeset
   350
            Antiquote.Text "" => ""
824d3f1d8de6 proper treatment of empty name -- avoid excessive vertical space;
wenzelm
parents: 42657
diff changeset
   351
          | Antiquote.Text s => output_text false s
42508
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   352
          | Antiquote.Antiq a => output_antiq a);
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   353
      in
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   354
        "\\rail@begin{" ^ string_of_int y' ^ "}{" ^ out_name ^ "}\n" ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   355
        output "" rail' ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   356
        "\\rail@end\n"
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   357
      end;
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   358
  in
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   359
    "\\begin{railoutput}\n" ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   360
    implode (map output_rule rules) ^
e21362bf1d93 allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents: 42507
diff changeset
   361
    "\\end{railoutput}\n"
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   362
  end;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   363
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   364
in
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   365
53171
a5e54d4d9081 added Theory.setup convenience;
wenzelm
parents: 48992
diff changeset
   366
val _ = Theory.setup
55030
9a9049d12e21 prefer user-space tool within Pure.thy;
wenzelm
parents: 55029
diff changeset
   367
  (Thy_Output.antiquotation @{binding rail}
55112
b1a5d603fd12 prefer rail cartouche -- avoid back-slashed quotes;
wenzelm
parents: 55030
diff changeset
   368
    (Scan.lift (Parse.source_position (Parse.string || Parse.cartouche)))
55613
ad446b45efff more markup;
wenzelm
parents: 55526
diff changeset
   369
    (fn {state, context, ...} => output_rules state o read context));
42504
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   370
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   371
end;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   372
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   373
end;
869c3f6f2d6e railroad diagrams in LaTeX as document antiquotation;
wenzelm
parents:
diff changeset
   374