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