author | wenzelm |
Thu, 05 Aug 2010 18:13:12 +0200 | |
changeset 38153 | 469555615ec7 |
parent 37982 | 111ce9651564 |
child 38767 | d8da44a8dd25 |
permissions | -rw-r--r-- |
32233 | 1 |
(* Title: doc-src/rail.ML |
2 |
Author: Michael Kerscher, TUM |
|
3 |
||
4 |
Railroad diagrams for LaTeX. |
|
5 |
*) |
|
6 |
||
7 |
structure Rail = |
|
8 |
struct |
|
9 |
||
32132 | 10 |
datatype token = |
11 |
Identifier of string | |
|
12 |
Special_Identifier of string | |
|
13 |
Text of string | |
|
14 |
Anot of string | |
|
15 |
Symbol of string | |
|
16 |
EOF; |
|
17 |
||
18 |
fun is_identifier (Identifier _) = true |
|
19 |
| is_identifier (Special_Identifier _ ) = true |
|
20 |
| is_identifier _ = false; |
|
32233 | 21 |
|
32132 | 22 |
fun is_text (Text _) = true |
23 |
| is_text _ = false; |
|
24 |
||
25 |
fun is_anot (Anot _) = true |
|
26 |
| is_anot _ = false; |
|
27 |
||
28 |
fun is_symbol (Symbol _) = true |
|
29 |
| is_symbol _ = false; |
|
30 |
||
31 |
fun is_ str = (fn s => s = Symbol str); |
|
32 |
||
33 |
||
34 |
local (* copied from antiquote-setup... *) |
|
35 |
fun translate f = Symbol.explode #> map f #> implode; |
|
36 |
||
37 |
fun clean_name "\<dots>" = "dots" |
|
38 |
| clean_name ".." = "ddot" |
|
39 |
| clean_name "." = "dot" |
|
40 |
| clean_name "_" = "underscore" |
|
41 |
| clean_name "{" = "braceleft" |
|
42 |
| clean_name "}" = "braceright" |
|
43 |
| clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c); |
|
44 |
||
45 |
fun no_check _ _ = true; |
|
46 |
||
47 |
fun false_check _ _ = false; |
|
48 |
||
49 |
fun thy_check intern defined ctxt = |
|
50 |
let val thy = ProofContext.theory_of ctxt |
|
51 |
in defined thy o intern thy end; |
|
52 |
||
53 |
fun check_tool name = |
|
54 |
File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name)); |
|
55 |
||
56 |
val arg = enclose "{" "}"; |
|
57 |
||
58 |
val markup_table = |
|
59 |
(* [(kind, (markup, check, style))*) |
|
60 |
Symtab.make [ |
|
61 |
("syntax", ("", no_check, true)), |
|
36973 | 62 |
("command", ("isacommand", K (is_some o Keyword.command_keyword), true)), |
63 |
("keyword", ("isakeyword", K Keyword.is_keyword, true)), |
|
64 |
("element", ("isakeyword", K Keyword.is_keyword, true)), |
|
32132 | 65 |
("method", ("", thy_check Method.intern Method.defined, true)), |
66 |
("attribute", ("", thy_check Attrib.intern Attrib.defined, true)), |
|
67 |
("fact", ("", no_check, true)), |
|
68 |
("variable", ("", no_check, true)), |
|
69 |
("case", ("", no_check, true)), |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36973
diff
changeset
|
70 |
("antiquotation", ("", K Thy_Output.defined_command, true)), |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36973
diff
changeset
|
71 |
("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *) |
32132 | 72 |
("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)), |
73 |
("inference", ("", no_check, true)), |
|
74 |
("executable", ("isatt", no_check, true)), |
|
75 |
("tool", ("isatt", K check_tool, true)), |
|
76 |
("file", ("isatt", K (File.exists o Path.explode), true)), |
|
37982 | 77 |
("theory", ("", K (can Thy_Info.get_theory), true)) |
32132 | 78 |
]; |
79 |
||
80 |
in |
|
81 |
||
82 |
fun decode_link ctxt (kind,index,logic,name) = |
|
83 |
let |
|
84 |
val (markup, check, style) = case Symtab.lookup markup_table kind of |
|
85 |
SOME x => x |
|
86 |
| NONE => ("", false_check, false); |
|
87 |
val hyper_name = |
|
88 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
89 |
val hyper = |
|
90 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
91 |
index = "def" ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
92 |
val idx = |
|
93 |
if index = "" then "" |
|
94 |
else "\\index" ^ index ^ arg logic ^ arg kind ^ arg name; |
|
95 |
in |
|
96 |
if check ctxt name then |
|
97 |
(idx ^ |
|
98 |
(Output.output name |
|
99 |
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36973
diff
changeset
|
100 |
|> (if ! Thy_Output.quotes then quote else I) |
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36973
diff
changeset
|
101 |
|> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
32449 | 102 |
else hyper o enclose "\\mbox{\\isa{" "}}")), style) |
32132 | 103 |
else ("Bad " ^ kind ^ " " ^ name, false) |
104 |
end; |
|
105 |
end; |
|
106 |
||
107 |
val blanks = |
|
108 |
Scan.many Symbol.is_blank >> implode; |
|
109 |
||
110 |
val scan_symbol = |
|
111 |
$$ ";" || $$ ":"|| $$ "("|| $$ ")"|| $$ "+"|| $$ "|"|| $$ "*"|| $$ "?"|| $$ "\\"; |
|
112 |
||
113 |
(* escaped version *) |
|
114 |
val scan_link = (* @{kind{_def|_ref (logic) name} *) |
|
115 |
let |
|
116 |
fun pseudo_antiquote inner_scan = ($$ "@" ^^ $$ "{") |-- inner_scan --| (blanks -- $$ "}"); |
|
117 |
fun parens scan = $$ "(" |-- scan --| $$ ")"; |
|
118 |
fun opt_quotes scan = $$ "'" |-- scan --| $$ "'" || scan; |
|
119 |
val letters = Scan.many Symbol.is_letter >> implode; |
|
120 |
val kind_name = letters; |
|
121 |
val opt_kind_type = Scan.optional ( |
|
122 |
$$ "_" |-- (Scan.this_string "def" || Scan.this_string "ref")) ""; |
|
123 |
val logic_name = letters; |
|
124 |
val escaped_singlequote = $$ "\\" |-- $$ "'"; |
|
125 |
val text = Scan.repeat (Scan.one Symbol.is_letter || escaped_singlequote) >> implode; |
|
126 |
in |
|
127 |
pseudo_antiquote ( |
|
128 |
kind_name -- opt_kind_type -- |
|
129 |
(blanks |-- Scan.optional ( parens logic_name ) "") -- |
|
130 |
(blanks |-- opt_quotes text) ) |
|
131 |
>> (fn (((kind,index),logic),name) => (kind, index, logic, name)) |
|
132 |
end; |
|
133 |
||
134 |
(* escaped version *) |
|
32233 | 135 |
fun scan_identifier ctxt = |
32132 | 136 |
let fun is_identifier_start s = |
137 |
Symbol.is_letter s orelse |
|
138 |
s = "_" |
|
139 |
fun is_identifier_rest s = |
|
140 |
Symbol.is_letter s orelse |
|
141 |
Symbol.is_digit s orelse |
|
142 |
s = "_" orelse |
|
143 |
s = "." |
|
144 |
in |
|
145 |
(Scan.one is_identifier_start ::: |
|
146 |
Scan.repeat (Scan.one is_identifier_rest || ($$ "\\" |-- $$ "'")) |
|
147 |
) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) || |
|
148 |
scan_link >> (decode_link ctxt) >> |
|
149 |
(fn (txt, style) => |
|
32449 | 150 |
if style then Special_Identifier(txt) |
151 |
else Identifier(txt)) |
|
32132 | 152 |
end; |
153 |
||
154 |
fun scan_anot ctxt = |
|
155 |
let val scan_anot = |
|
156 |
Scan.many (fn s => |
|
157 |
s <> "\n" andalso |
|
158 |
s <> "\t" andalso |
|
159 |
s <> "]" andalso |
|
160 |
Symbol.is_regular s) >> implode |
|
161 |
in |
|
162 |
$$ "[" |-- scan_link --| $$ "]" >> (fst o (decode_link ctxt)) || |
|
163 |
$$ "[" |-- scan_anot --| $$ "]" >> Output.output |
|
164 |
end; |
|
165 |
||
166 |
(* escaped version *) |
|
167 |
fun scan_text ctxt = |
|
168 |
let |
|
169 |
val text_sq = |
|
170 |
Scan.repeat ( |
|
171 |
Scan.one (fn s => |
|
32449 | 172 |
s <> "\n" andalso |
173 |
s <> "\t" andalso |
|
174 |
s <> "'" andalso |
|
175 |
s <> "\\" andalso |
|
176 |
Symbol.is_regular s) || |
|
177 |
($$ "\\" |-- $$ "'") |
|
32132 | 178 |
) >> implode |
179 |
fun quoted scan = $$ "'" |-- scan --| $$ "'"; |
|
180 |
in |
|
181 |
quoted scan_link >> (fst o (decode_link ctxt)) || |
|
182 |
quoted text_sq >> (enclose "\\isa{" "}" o Output.output) |
|
183 |
end; |
|
184 |
||
185 |
fun scan_rail ctxt = |
|
186 |
Scan.repeat ( blanks |-- ( |
|
187 |
scan_identifier ctxt || |
|
188 |
scan_anot ctxt >> Anot || |
|
189 |
scan_text ctxt >> Text || |
|
190 |
scan_symbol >> Symbol) |
|
191 |
) --| blanks; |
|
192 |
||
193 |
fun lex_rail txt ctxt = (* Symbol_Pos fuer spaeter durchgereicht *) |
|
194 |
Symbol.scanner "Malformed rail-declaration" (scan_rail ctxt) (map fst (Symbol_Pos.explode txt)); |
|
195 |
||
196 |
val lex = lex_rail; |
|
197 |
||
198 |
datatype id_kind = UNKNOWN | TOKEN | TERM | NTERM; |
|
199 |
||
200 |
datatype id_type = |
|
201 |
Id of string * id_kind | |
|
202 |
Null_Id; |
|
203 |
||
204 |
datatype body_kind = |
|
205 |
CAT | BAR | PLUS | |
|
206 |
CR | EMPTY | ANNOTE | IDENT | STRING | |
|
207 |
Null_Kind; |
|
208 |
||
32233 | 209 |
datatype body_type = |
32132 | 210 |
Body of body_kind * string * string * id_type * body_type list | |
211 |
Body_Pos of body_kind * string * string * id_type * body_type list * int * int | |
|
212 |
Empty_Body | |
|
213 |
Null_Body; |
|
214 |
||
32233 | 215 |
datatype rule = |
32132 | 216 |
Rule of id_type * body_type; |
217 |
||
218 |
fun new_id id kind = Id (id, kind); |
|
219 |
||
220 |
fun is_empty (Body(kind,_,_,_,_)) = kind = EMPTY; |
|
221 |
||
222 |
fun new_body (kind, Null_Body, Null_Body) = Body (kind, "", "", Null_Id, []) |
|
223 |
| new_body (kind, body1, body2) = Body (kind, "", "", Null_Id, body1 :: [body2]); |
|
224 |
||
225 |
fun is_kind_of kind (Body(bodyKind,_,_,_,_)) = kind = bodyKind |
|
226 |
| is_kind_of _ _ = false; |
|
227 |
||
228 |
fun add_list (Body(kind, text, annot, id, bodies), body) = |
|
229 |
Body(kind, text, annot, id, bodies @ [body]); |
|
230 |
||
32233 | 231 |
fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) = |
32132 | 232 |
Body(kind, text, annot, id, bodies1 @ bodies2); |
233 |
||
234 |
fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) = |
|
235 |
if kind = kind1 andalso kind <> BAR then |
|
236 |
if kind = kind2 then |
|
237 |
cat_body_lists(body1, body2) |
|
238 |
else (* kind <> kind2 *) |
|
239 |
add_list(body1, body2) |
|
240 |
else (* kind <> kind1 orelse kind = BAR *) |
|
241 |
if kind = kind2 then |
|
242 |
cat_body_lists(add_list(new_body(kind,Null_Body,Null_Body), body1), body2) |
|
243 |
else (* kind <> kind2 *) |
|
244 |
add_list(add_list(new_body(kind,Null_Body,Null_Body), body1), body2); |
|
245 |
||
246 |
fun rev_body (body as Body (kind, text, annot, id, [])) = body |
|
247 |
| rev_body (Body (CAT, text, annot, id, bodies)) = |
|
248 |
Body(CAT, text, annot, id, map rev_body (rev bodies)) |
|
249 |
| rev_body (Body (kind, text, annot, id, bodies)) = |
|
250 |
Body(kind, text, annot, id, map rev_body bodies) |
|
251 |
| rev_body body = body; |
|
252 |
||
253 |
fun set_body_text text (Body(k,_,a,i,b)) = Body(k,text,a,i,b); |
|
254 |
fun set_body_anot anot (Body(k,t,_,i,b)) = Body(k,t,anot,i,b); |
|
255 |
fun set_body_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TOKEN,b); |
|
256 |
fun set_body_special_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TERM,b); |
|
257 |
||
258 |
||
259 |
fun mk_eof _ = EOF; |
|
260 |
fun is_eof s = s = EOF; |
|
261 |
val stopper = Scan.stopper mk_eof is_eof; |
|
262 |
||
263 |
(* TODO: change this, so the next or next two tokens are printed *) |
|
264 |
fun lex_err msg (cs, _) = "rail grammar error: " ^ msg cs; |
|
265 |
fun !!! msg scan = Scan.!! (lex_err (K msg)) scan; |
|
266 |
fun $$$ tok = Scan.one (is_ tok); |
|
267 |
||
268 |
||
269 |
local |
|
270 |
fun new_bar_body([], body2) = body2 |
|
271 |
| new_bar_body(body1::bodies, body2) = |
|
272 |
add_body(BAR, body1, new_bar_body(bodies, body2)); |
|
273 |
||
274 |
fun new_cat_body(body::[]) = body |
|
275 |
| new_cat_body(body1::bodies) = add_body(CAT, body1, new_cat_body(bodies)); |
|
276 |
||
277 |
fun new_annote_body (Anot anot) = |
|
278 |
set_body_text anot (new_body(ANNOTE, Empty_Body, Empty_Body)); |
|
279 |
||
280 |
fun new_text_annote_body (Text text, Anot anot) = |
|
281 |
set_body_anot anot (set_body_text text (new_body(STRING, Empty_Body, Empty_Body))); |
|
282 |
||
283 |
fun new_ident_body (Identifier ident, Anot anot) = |
|
284 |
set_body_anot anot (set_body_ident ident (new_body(IDENT, Empty_Body, Empty_Body))) |
|
285 |
| new_ident_body (Special_Identifier ident, Anot anot) = |
|
286 |
set_body_anot anot (set_body_special_ident ident (new_body(IDENT, Empty_Body, Empty_Body))); |
|
287 |
||
288 |
val new_empty_body = new_body(EMPTY, Null_Body, Null_Body); |
|
289 |
in |
|
290 |
||
291 |
fun parse_body x = |
|
292 |
( |
|
293 |
Scan.repeat1 (parse_body0 --| $$$ "|") -- !!! "body0 expected" (parse_body0) >> |
|
294 |
new_bar_body || |
|
295 |
parse_body0 |
|
296 |
) x |
|
297 |
and parse_body0 x = |
|
298 |
( |
|
299 |
Scan.one is_anot -- !!! "body1 expected" (parse_body1) >> |
|
300 |
(fn (anot, body) => add_body(CAT, new_annote_body(anot), body)) || |
|
301 |
parse_body1 |
|
302 |
) x |
|
303 |
and parse_body1 x = |
|
304 |
( |
|
305 |
parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >> |
|
306 |
(fn (body1, body2) => |
|
307 |
if is_empty body2 then |
|
32449 | 308 |
add_body(PLUS, new_empty_body, rev_body body1) |
32132 | 309 |
else |
32449 | 310 |
add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) || |
32233 | 311 |
parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >> |
32132 | 312 |
(fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) || |
313 |
parse_body2e |
|
314 |
) x |
|
315 |
and parse_body2e x = |
|
316 |
( |
|
317 |
parse_body2 || |
|
318 |
(fn toks => (new_empty_body, toks)) |
|
319 |
) x |
|
320 |
and parse_body2 x = |
|
321 |
( |
|
322 |
Scan.repeat1 (parse_body3) >> new_cat_body |
|
323 |
) x |
|
324 |
and parse_body3 x = |
|
325 |
( |
|
326 |
parse_body4 --| $$$ "?" >> (fn body => new_body (BAR, new_empty_body, body) ) || |
|
327 |
parse_body4 |
|
328 |
) x |
|
329 |
and parse_body4e x = |
|
330 |
( |
|
331 |
parse_body4 || |
|
332 |
(fn toks => (new_empty_body, toks)) |
|
333 |
) x |
|
334 |
and parse_body4 x = |
|
335 |
( |
|
336 |
$$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") || |
|
337 |
Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >> |
|
32233 | 338 |
(fn (text, anot) => new_text_annote_body (text,anot)) || |
32132 | 339 |
Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >> |
340 |
(fn (id, anot) => new_ident_body (id,anot)) || |
|
341 |
$$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body)) |
|
342 |
) x; |
|
343 |
end; |
|
344 |
||
345 |
fun new_named_rule (Identifier name, body) = Rule(Id(name, UNKNOWN), body) |
|
346 |
| new_named_rule (Special_Identifier name, body) = Rule(Id(name, UNKNOWN), body); |
|
347 |
fun new_anonym_rule body = Rule(Null_Id, body); |
|
348 |
||
349 |
val parse_rule = |
|
350 |
(Scan.one (is_identifier) -- ($$$ ":" |-- !!! "body expected" (parse_body)) ) >> |
|
351 |
new_named_rule || |
|
352 |
parse_body >> new_anonym_rule; |
|
353 |
||
354 |
val parse_rules = |
|
355 |
Scan.repeat ( parse_rule --| $$$ ";") @@@ Scan.single parse_rule; |
|
356 |
||
357 |
fun parse_rail s = |
|
358 |
Scan.read stopper parse_rules s; |
|
359 |
||
360 |
val parse = parse_rail; |
|
361 |
||
362 |
fun getystart (Body_Pos(_,_,_,_,_,ystart,_)) = ystart; |
|
363 |
fun getynext (Body_Pos(_,_,_,_,_,_,ynext)) = ynext; |
|
364 |
||
365 |
fun position_body (body as Body(kind, text, annot, id, bodies), ystart) = |
|
366 |
let fun max (x,y) = if x > y then x else y |
|
367 |
fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) = |
|
32449 | 368 |
Body_Pos(kind, text, annot, id, bodies, ystart, ynext) |
32132 | 369 |
fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext) |
370 |
| pos_bodies_cat (x::xs, ystart, ynext, liste) = |
|
32449 | 371 |
if is_kind_of CR x then |
372 |
(case set_body_position(x, ystart, ynext+1) of |
|
373 |
body as Body_Pos(_,_,_,_,_,_,ynext1) => |
|
374 |
pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body]) |
|
375 |
) |
|
376 |
else |
|
377 |
(case position_body(x, ystart) of |
|
378 |
body as Body_Pos(_,_,_,_,_,_,ynext1) => |
|
379 |
pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body]) |
|
380 |
) |
|
32132 | 381 |
fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext) |
382 |
| pos_bodies_bar_plus (x::xs, ystart, ynext, liste) = |
|
32449 | 383 |
(case position_body(x, ystart) of |
384 |
body as Body_Pos(_,_,_,_,_,_,ynext1) => |
|
385 |
pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body]) |
|
386 |
) |
|
32132 | 387 |
in |
388 |
(case kind of |
|
389 |
CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of |
|
32449 | 390 |
(bodiesPos, ynext) => |
391 |
Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext)) |
|
32132 | 392 |
| BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of |
32449 | 393 |
(bodiesPos, ynext) => |
394 |
Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext)) |
|
32132 | 395 |
| PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of |
32449 | 396 |
(bodiesPos, ynext) => |
397 |
Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext)) |
|
32132 | 398 |
| CR => set_body_position(body, ystart, ystart+3) |
399 |
| EMPTY => set_body_position(body, ystart, ystart+1) |
|
400 |
| ANNOTE => set_body_position(body, ystart, ystart+1) |
|
401 |
| IDENT => set_body_position(body, ystart, ystart+1) |
|
402 |
| STRING => set_body_position(body, ystart, ystart+1) |
|
403 |
) |
|
404 |
end; |
|
405 |
||
406 |
fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = "" |
|
407 |
| format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) = |
|
408 |
let fun format_bodies([]) = "" |
|
32449 | 409 |
| format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs) |
32132 | 410 |
in |
411 |
format_bodies(bodies) |
|
412 |
end |
|
32233 | 413 |
| format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) = |
32132 | 414 |
let fun format_bodies([]) = "\\rail@endbar\n" |
32449 | 415 |
| format_bodies(x::xs) = |
416 |
"\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^ |
|
417 |
format_body(x, "") ^ format_bodies(xs) |
|
32132 | 418 |
in |
419 |
"\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies)) |
|
420 |
end |
|
421 |
| format_body (Body_Pos(PLUS,_,_,_,x::y::xs,_,_),cent) = |
|
422 |
"\\rail@plus\n" ^ format_body(x, cent) ^ |
|
423 |
"\\rail@nextplus{" ^ string_of_int(getystart(y)) ^ "}\n" ^ |
|
424 |
format_body(y, "c") ^ |
|
425 |
"\\rail@endplus\n" |
|
426 |
| format_body (Body_Pos(ANNOTE,text,_,_,_,_,_),cent) = |
|
427 |
"\\rail@annote[" ^ text ^ "]\n" |
|
428 |
| format_body (Body_Pos(IDENT,_,annot,Id(name,TERM),_,_,_),cent) = |
|
429 |
"\\rail@" ^ cent ^ "token{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n" |
|
430 |
| format_body (Body_Pos(IDENT,_,annot,Id(name,_),_,_,_),cent) = |
|
431 |
"\\rail@" ^ cent ^ "nont{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n" |
|
432 |
| format_body (Body_Pos(CR,_,_,_,_,_,ynext),cent) = |
|
433 |
"\\rail@cr{" ^ string_of_int(ynext) ^ "}\n" |
|
434 |
| format_body (Body_Pos(STRING,text,annot,_,_,_,_),cent) = |
|
435 |
"\\rail@" ^ cent ^ "term{" ^ text ^ "}[" ^ annot ^ "]\n" |
|
436 |
| format_body _ = |
|
437 |
"\\rail@unknown\n"; |
|
438 |
||
439 |
fun out_body (Id(name,_), body) = |
|
440 |
let val bodyPos as Body_Pos(_,_,_,_,_,_,ynext) = position_body(body,0) |
|
441 |
in |
|
442 |
"\\rail@begin{" ^ string_of_int(ynext) ^ "}{" ^ name ^ "}\n" ^ |
|
443 |
format_body(bodyPos,"") ^ |
|
444 |
"\\rail@end\n" |
|
445 |
end |
|
446 |
| out_body (Null_Id, body) = out_body (Id("", UNKNOWN), body); |
|
447 |
||
448 |
fun out_rule (Rule(id, body)) = |
|
449 |
if is_empty body then "" |
|
450 |
else out_body (id, body); |
|
451 |
||
452 |
fun out_rules ([]) = "" |
|
453 |
| out_rules (rule::rules) = out_rule rule ^ out_rules rules; |
|
454 |
||
455 |
val output_no_rules = |
|
456 |
"\\rail@begin{1}{}\n" ^ |
|
457 |
"\\rail@setbox{\\bfseries ???}\n" ^ |
|
458 |
"\\rail@oval\n" ^ |
|
459 |
"\\rail@end\n"; |
|
460 |
||
461 |
||
462 |
fun print (SOME rules) = |
|
463 |
"\\begin{railoutput}\n" ^ |
|
464 |
out_rules rules ^ |
|
465 |
"\\end{railoutput}\n" |
|
466 |
| print (NONE) = |
|
467 |
"\\begin{railoutput}\n" ^ |
|
468 |
output_no_rules ^ |
|
469 |
"\\end{railoutput}\n"; |
|
470 |
||
471 |
fun process txt ctxt = |
|
472 |
lex txt ctxt |
|
473 |
|> parse |
|
474 |
|> print; |
|
475 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36973
diff
changeset
|
476 |
val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name)) |
32132 | 477 |
(fn {context = ctxt,...} => fn txt => process txt ctxt); |
32233 | 478 |
|
479 |
end; |
|
480 |