1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/rail.ML Wed Jul 22 11:48:04 2009 +0200
1.3 @@ -0,0 +1,468 @@
1.4 +datatype token =
1.5 + Identifier of string |
1.6 + Special_Identifier of string |
1.7 + Text of string |
1.8 + Anot of string |
1.9 + Symbol of string |
1.10 + EOF;
1.11 +
1.12 +fun is_identifier (Identifier _) = true
1.13 + | is_identifier (Special_Identifier _ ) = true
1.14 + | is_identifier _ = false;
1.15 +
1.16 +fun is_text (Text _) = true
1.17 + | is_text _ = false;
1.18 +
1.19 +fun is_anot (Anot _) = true
1.20 + | is_anot _ = false;
1.21 +
1.22 +fun is_symbol (Symbol _) = true
1.23 + | is_symbol _ = false;
1.24 +
1.25 +fun is_ str = (fn s => s = Symbol str);
1.26 +
1.27 +
1.28 +local (* copied from antiquote-setup... *)
1.29 +fun translate f = Symbol.explode #> map f #> implode;
1.30 +
1.31 +fun clean_name "\<dots>" = "dots"
1.32 + | clean_name ".." = "ddot"
1.33 + | clean_name "." = "dot"
1.34 + | clean_name "_" = "underscore"
1.35 + | clean_name "{" = "braceleft"
1.36 + | clean_name "}" = "braceright"
1.37 + | clean_name s = s |> translate (fn "_" => "-" | "\<dash>" => "-" | c => c);
1.38 +
1.39 +fun no_check _ _ = true;
1.40 +
1.41 +fun false_check _ _ = false;
1.42 +
1.43 +fun thy_check intern defined ctxt =
1.44 + let val thy = ProofContext.theory_of ctxt
1.45 + in defined thy o intern thy end;
1.46 +
1.47 +fun check_tool name =
1.48 + File.exists (Path.append (Path.explode "~~/lib/Tools") (Path.basic name));
1.49 +
1.50 +val arg = enclose "{" "}";
1.51 +
1.52 +val markup_table =
1.53 +(* [(kind, (markup, check, style))*)
1.54 + Symtab.make [
1.55 + ("syntax", ("", no_check, true)),
1.56 + ("command", ("isacommand", K (is_some o OuterKeyword.command_keyword), true)),
1.57 + ("keyword", ("isakeyword", K OuterKeyword.is_keyword, true)),
1.58 + ("element", ("isakeyword", K OuterKeyword.is_keyword, true)),
1.59 + ("method", ("", thy_check Method.intern Method.defined, true)),
1.60 + ("attribute", ("", thy_check Attrib.intern Attrib.defined, true)),
1.61 + ("fact", ("", no_check, true)),
1.62 + ("variable", ("", no_check, true)),
1.63 + ("case", ("", no_check, true)),
1.64 + ("antiquotation", ("", K ThyOutput.defined_command, true)),
1.65 + ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
1.66 + ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
1.67 + ("inference", ("", no_check, true)),
1.68 + ("executable", ("isatt", no_check, true)),
1.69 + ("tool", ("isatt", K check_tool, true)),
1.70 + ("file", ("isatt", K (File.exists o Path.explode), true)),
1.71 + ("theory", ("", K ThyInfo.known_thy, true))
1.72 + ];
1.73 +
1.74 +in
1.75 +
1.76 +fun decode_link ctxt (kind,index,logic,name) =
1.77 + let
1.78 + val (markup, check, style) = case Symtab.lookup markup_table kind of
1.79 + SOME x => x
1.80 + | NONE => ("", false_check, false);
1.81 + val hyper_name =
1.82 + "{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}";
1.83 + val hyper =
1.84 + enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
1.85 + index = "def" ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
1.86 + val idx =
1.87 + if index = "" then ""
1.88 + else "\\index" ^ index ^ arg logic ^ arg kind ^ arg name;
1.89 + in
1.90 + if check ctxt name then
1.91 + (idx ^
1.92 + (Output.output name
1.93 + |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
1.94 + |> (if ! ThyOutput.quotes then quote else I)
1.95 + |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
1.96 + else hyper o enclose "\\mbox{\\isa{" "}}")), style)
1.97 + else ("Bad " ^ kind ^ " " ^ name, false)
1.98 + end;
1.99 +end;
1.100 +
1.101 +val blanks =
1.102 + Scan.many Symbol.is_blank >> implode;
1.103 +
1.104 +val scan_symbol =
1.105 + $$ ";" || $$ ":"|| $$ "("|| $$ ")"|| $$ "+"|| $$ "|"|| $$ "*"|| $$ "?"|| $$ "\\";
1.106 +
1.107 +(* escaped version *)
1.108 +val scan_link = (* @{kind{_def|_ref (logic) name} *)
1.109 + let
1.110 + fun pseudo_antiquote inner_scan = ($$ "@" ^^ $$ "{") |-- inner_scan --| (blanks -- $$ "}");
1.111 + fun parens scan = $$ "(" |-- scan --| $$ ")";
1.112 + fun opt_quotes scan = $$ "'" |-- scan --| $$ "'" || scan;
1.113 + val letters = Scan.many Symbol.is_letter >> implode;
1.114 + val kind_name = letters;
1.115 + val opt_kind_type = Scan.optional (
1.116 + $$ "_" |-- (Scan.this_string "def" || Scan.this_string "ref")) "";
1.117 + val logic_name = letters;
1.118 + val escaped_singlequote = $$ "\\" |-- $$ "'";
1.119 + val text = Scan.repeat (Scan.one Symbol.is_letter || escaped_singlequote) >> implode;
1.120 + in
1.121 + pseudo_antiquote (
1.122 + kind_name -- opt_kind_type --
1.123 + (blanks |-- Scan.optional ( parens logic_name ) "") --
1.124 + (blanks |-- opt_quotes text) )
1.125 + >> (fn (((kind,index),logic),name) => (kind, index, logic, name))
1.126 +end;
1.127 +
1.128 +(* escaped version *)
1.129 +fun scan_identifier ctxt =
1.130 + let fun is_identifier_start s =
1.131 + Symbol.is_letter s orelse
1.132 + s = "_"
1.133 + fun is_identifier_rest s =
1.134 + Symbol.is_letter s orelse
1.135 + Symbol.is_digit s orelse
1.136 + s = "_" orelse
1.137 + s = "."
1.138 + in
1.139 + (Scan.one is_identifier_start :::
1.140 + Scan.repeat (Scan.one is_identifier_rest || ($$ "\\" |-- $$ "'"))
1.141 + ) >> (Identifier o enclose "\\isa{" "}" o Output.output o implode) ||
1.142 + scan_link >> (decode_link ctxt) >>
1.143 + (fn (txt, style) =>
1.144 + if style then Special_Identifier(txt)
1.145 + else Identifier(txt))
1.146 +end;
1.147 +
1.148 +fun scan_anot ctxt =
1.149 + let val scan_anot =
1.150 + Scan.many (fn s =>
1.151 + s <> "\n" andalso
1.152 + s <> "\t" andalso
1.153 + s <> "]" andalso
1.154 + Symbol.is_regular s) >> implode
1.155 + in
1.156 + $$ "[" |-- scan_link --| $$ "]" >> (fst o (decode_link ctxt)) ||
1.157 + $$ "[" |-- scan_anot --| $$ "]" >> Output.output
1.158 +end;
1.159 +
1.160 +(* escaped version *)
1.161 +fun scan_text ctxt =
1.162 + let
1.163 + val text_sq =
1.164 + Scan.repeat (
1.165 + Scan.one (fn s =>
1.166 + s <> "\n" andalso
1.167 + s <> "\t" andalso
1.168 + s <> "'" andalso
1.169 + s <> "\\" andalso
1.170 + Symbol.is_regular s) ||
1.171 + ($$ "\\" |-- $$ "'")
1.172 + ) >> implode
1.173 + fun quoted scan = $$ "'" |-- scan --| $$ "'";
1.174 + in
1.175 + quoted scan_link >> (fst o (decode_link ctxt)) ||
1.176 + quoted text_sq >> (enclose "\\isa{" "}" o Output.output)
1.177 +end;
1.178 +
1.179 +fun scan_rail ctxt =
1.180 + Scan.repeat ( blanks |-- (
1.181 + scan_identifier ctxt ||
1.182 + scan_anot ctxt >> Anot ||
1.183 + scan_text ctxt >> Text ||
1.184 + scan_symbol >> Symbol)
1.185 + ) --| blanks;
1.186 +
1.187 +fun lex_rail txt ctxt = (* Symbol_Pos fuer spaeter durchgereicht *)
1.188 + Symbol.scanner "Malformed rail-declaration" (scan_rail ctxt) (map fst (Symbol_Pos.explode txt));
1.189 +
1.190 +val lex = lex_rail;
1.191 +
1.192 +datatype id_kind = UNKNOWN | TOKEN | TERM | NTERM;
1.193 +
1.194 +datatype id_type =
1.195 + Id of string * id_kind |
1.196 + Null_Id;
1.197 +
1.198 +datatype body_kind =
1.199 + CAT | BAR | PLUS |
1.200 + CR | EMPTY | ANNOTE | IDENT | STRING |
1.201 + Null_Kind;
1.202 +
1.203 +datatype body_type =
1.204 + Body of body_kind * string * string * id_type * body_type list |
1.205 + Body_Pos of body_kind * string * string * id_type * body_type list * int * int |
1.206 + Empty_Body |
1.207 + Null_Body;
1.208 +
1.209 +datatype rule =
1.210 + Rule of id_type * body_type;
1.211 +
1.212 +fun new_id id kind = Id (id, kind);
1.213 +
1.214 +fun is_empty (Body(kind,_,_,_,_)) = kind = EMPTY;
1.215 +
1.216 +fun new_body (kind, Null_Body, Null_Body) = Body (kind, "", "", Null_Id, [])
1.217 + | new_body (kind, body1, body2) = Body (kind, "", "", Null_Id, body1 :: [body2]);
1.218 +
1.219 +fun is_kind_of kind (Body(bodyKind,_,_,_,_)) = kind = bodyKind
1.220 + | is_kind_of _ _ = false;
1.221 +
1.222 +fun add_list (Body(kind, text, annot, id, bodies), body) =
1.223 + Body(kind, text, annot, id, bodies @ [body]);
1.224 +
1.225 +fun cat_body_lists (Body(kind, text, annot, id, bodies1), Body(_,_,_,_, bodies2)) =
1.226 + Body(kind, text, annot, id, bodies1 @ bodies2);
1.227 +
1.228 +fun add_body (kind, body1 as Body(kind1,_,_,_,_), body2 as Body(kind2,_,_,_,_)) =
1.229 + if kind = kind1 andalso kind <> BAR then
1.230 + if kind = kind2 then
1.231 + cat_body_lists(body1, body2)
1.232 + else (* kind <> kind2 *)
1.233 + add_list(body1, body2)
1.234 + else (* kind <> kind1 orelse kind = BAR *)
1.235 + if kind = kind2 then
1.236 + cat_body_lists(add_list(new_body(kind,Null_Body,Null_Body), body1), body2)
1.237 + else (* kind <> kind2 *)
1.238 + add_list(add_list(new_body(kind,Null_Body,Null_Body), body1), body2);
1.239 +
1.240 +fun rev_body (body as Body (kind, text, annot, id, [])) = body
1.241 + | rev_body (Body (CAT, text, annot, id, bodies)) =
1.242 + Body(CAT, text, annot, id, map rev_body (rev bodies))
1.243 + | rev_body (Body (kind, text, annot, id, bodies)) =
1.244 + Body(kind, text, annot, id, map rev_body bodies)
1.245 + | rev_body body = body;
1.246 +
1.247 +fun set_body_text text (Body(k,_,a,i,b)) = Body(k,text,a,i,b);
1.248 +fun set_body_anot anot (Body(k,t,_,i,b)) = Body(k,t,anot,i,b);
1.249 +fun set_body_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TOKEN,b);
1.250 +fun set_body_special_ident id (Body(k,t,a,_,b)) = Body(k,t,a, new_id id TERM,b);
1.251 +
1.252 +
1.253 +fun mk_eof _ = EOF;
1.254 +fun is_eof s = s = EOF;
1.255 +val stopper = Scan.stopper mk_eof is_eof;
1.256 +
1.257 +(* TODO: change this, so the next or next two tokens are printed *)
1.258 +fun lex_err msg (cs, _) = "rail grammar error: " ^ msg cs;
1.259 +fun !!! msg scan = Scan.!! (lex_err (K msg)) scan;
1.260 +fun $$$ tok = Scan.one (is_ tok);
1.261 +
1.262 +
1.263 +local
1.264 +fun new_bar_body([], body2) = body2
1.265 + | new_bar_body(body1::bodies, body2) =
1.266 + add_body(BAR, body1, new_bar_body(bodies, body2));
1.267 +
1.268 +fun new_cat_body(body::[]) = body
1.269 + | new_cat_body(body1::bodies) = add_body(CAT, body1, new_cat_body(bodies));
1.270 +
1.271 +fun new_annote_body (Anot anot) =
1.272 + set_body_text anot (new_body(ANNOTE, Empty_Body, Empty_Body));
1.273 +
1.274 +fun new_text_annote_body (Text text, Anot anot) =
1.275 + set_body_anot anot (set_body_text text (new_body(STRING, Empty_Body, Empty_Body)));
1.276 +
1.277 +fun new_ident_body (Identifier ident, Anot anot) =
1.278 + set_body_anot anot (set_body_ident ident (new_body(IDENT, Empty_Body, Empty_Body)))
1.279 + | new_ident_body (Special_Identifier ident, Anot anot) =
1.280 + set_body_anot anot (set_body_special_ident ident (new_body(IDENT, Empty_Body, Empty_Body)));
1.281 +
1.282 +val new_empty_body = new_body(EMPTY, Null_Body, Null_Body);
1.283 +in
1.284 +
1.285 +fun parse_body x =
1.286 + (
1.287 + Scan.repeat1 (parse_body0 --| $$$ "|") -- !!! "body0 expected" (parse_body0) >>
1.288 + new_bar_body ||
1.289 + parse_body0
1.290 + ) x
1.291 +and parse_body0 x =
1.292 + (
1.293 + Scan.one is_anot -- !!! "body1 expected" (parse_body1) >>
1.294 + (fn (anot, body) => add_body(CAT, new_annote_body(anot), body)) ||
1.295 + parse_body1
1.296 + ) x
1.297 +and parse_body1 x =
1.298 + (
1.299 + parse_body2 -- ($$$ "*" |-- !!! "body4e expected" (parse_body4e)) >>
1.300 + (fn (body1, body2) =>
1.301 + if is_empty body2 then
1.302 + add_body(PLUS, new_empty_body, rev_body body1)
1.303 + else
1.304 + add_body(BAR, new_empty_body, add_body (PLUS, body1, rev_body body2)) ) ||
1.305 + parse_body2 -- ($$$ "+" |-- !!! "body4e expected" (parse_body4e)) >>
1.306 + (fn (body1, body2) => new_body (PLUS, body1, rev_body body2) ) ||
1.307 + parse_body2e
1.308 + ) x
1.309 +and parse_body2e x =
1.310 + (
1.311 + parse_body2 ||
1.312 + (fn toks => (new_empty_body, toks))
1.313 + ) x
1.314 +and parse_body2 x =
1.315 + (
1.316 + Scan.repeat1 (parse_body3) >> new_cat_body
1.317 + ) x
1.318 +and parse_body3 x =
1.319 + (
1.320 + parse_body4 --| $$$ "?" >> (fn body => new_body (BAR, new_empty_body, body) ) ||
1.321 + parse_body4
1.322 + ) x
1.323 +and parse_body4e x =
1.324 + (
1.325 + parse_body4 ||
1.326 + (fn toks => (new_empty_body, toks))
1.327 + ) x
1.328 +and parse_body4 x =
1.329 + (
1.330 + $$$ "(" |-- !!! "body0 or ')' expected" (parse_body --| $$$ ")") ||
1.331 + Scan.one is_text -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
1.332 + (fn (text, anot) => new_text_annote_body (text,anot)) ||
1.333 + Scan.one is_identifier -- (Scan.optional (Scan.one is_anot) (Anot(""))) >>
1.334 + (fn (id, anot) => new_ident_body (id,anot)) ||
1.335 + $$$ "\\" >> (fn _ => new_body (CR, Null_Body, Null_Body))
1.336 + ) x;
1.337 +end;
1.338 +
1.339 +fun new_named_rule (Identifier name, body) = Rule(Id(name, UNKNOWN), body)
1.340 + | new_named_rule (Special_Identifier name, body) = Rule(Id(name, UNKNOWN), body);
1.341 +fun new_anonym_rule body = Rule(Null_Id, body);
1.342 +
1.343 +val parse_rule =
1.344 + (Scan.one (is_identifier) -- ($$$ ":" |-- !!! "body expected" (parse_body)) ) >>
1.345 + new_named_rule ||
1.346 + parse_body >> new_anonym_rule;
1.347 +
1.348 +val parse_rules =
1.349 + Scan.repeat ( parse_rule --| $$$ ";") @@@ Scan.single parse_rule;
1.350 +
1.351 +fun parse_rail s =
1.352 + Scan.read stopper parse_rules s;
1.353 +
1.354 +val parse = parse_rail;
1.355 +
1.356 +fun getystart (Body_Pos(_,_,_,_,_,ystart,_)) = ystart;
1.357 +fun getynext (Body_Pos(_,_,_,_,_,_,ynext)) = ynext;
1.358 +
1.359 +fun position_body (body as Body(kind, text, annot, id, bodies), ystart) =
1.360 + let fun max (x,y) = if x > y then x else y
1.361 + fun set_body_position (Body(kind, text, annot, id, bodies), ystart, ynext) =
1.362 + Body_Pos(kind, text, annot, id, bodies, ystart, ynext)
1.363 + fun pos_bodies_cat ([],_,ynext,liste) = (liste, ynext)
1.364 + | pos_bodies_cat (x::xs, ystart, ynext, liste) =
1.365 + if is_kind_of CR x then
1.366 + (case set_body_position(x, ystart, ynext+1) of
1.367 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.368 + pos_bodies_cat(xs, ynext1, max(ynext,ynext1), liste@[body])
1.369 + )
1.370 + else
1.371 + (case position_body(x, ystart) of
1.372 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.373 + pos_bodies_cat(xs, ystart, max(ynext,ynext1), liste@[body])
1.374 + )
1.375 + fun pos_bodies_bar_plus ([],_,ynext,liste) = (liste, ynext)
1.376 + | pos_bodies_bar_plus (x::xs, ystart, ynext, liste) =
1.377 + (case position_body(x, ystart) of
1.378 + body as Body_Pos(_,_,_,_,_,_,ynext1) =>
1.379 + pos_bodies_bar_plus(xs, ynext1, max(ynext,ynext1), liste@[body])
1.380 + )
1.381 + in
1.382 + (case kind of
1.383 + CAT => (case pos_bodies_cat(bodies,ystart,ystart+1,[]) of
1.384 + (bodiesPos, ynext) =>
1.385 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.386 + | BAR => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
1.387 + (bodiesPos, ynext) =>
1.388 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.389 + | PLUS => (case pos_bodies_bar_plus(bodies,ystart,ystart+1,[]) of
1.390 + (bodiesPos, ynext) =>
1.391 + Body_Pos(kind, text, annot, id, bodiesPos, ystart, ynext))
1.392 + | CR => set_body_position(body, ystart, ystart+3)
1.393 + | EMPTY => set_body_position(body, ystart, ystart+1)
1.394 + | ANNOTE => set_body_position(body, ystart, ystart+1)
1.395 + | IDENT => set_body_position(body, ystart, ystart+1)
1.396 + | STRING => set_body_position(body, ystart, ystart+1)
1.397 + )
1.398 + end;
1.399 +
1.400 +fun format_body (Body_Pos(EMPTY,_,_,_,_,_,_), _) = ""
1.401 + | format_body (Body_Pos(CAT,_,_,_,bodies,_,_), cent) =
1.402 + let fun format_bodies([]) = ""
1.403 + | format_bodies(x::xs) = format_body (x, "") ^ format_bodies(xs)
1.404 + in
1.405 + format_bodies(bodies)
1.406 + end
1.407 + | format_body (Body_Pos(BAR,_,_,_,bodies,_,_),cent) =
1.408 + let fun format_bodies([]) = "\\rail@endbar\n"
1.409 + | format_bodies(x::xs) =
1.410 + "\\rail@nextbar{" ^ string_of_int(getystart(x)) ^"}\n" ^
1.411 + format_body(x, "") ^ format_bodies(xs)
1.412 + in
1.413 + "\\rail@bar\n" ^ format_body(hd(bodies), "") ^ format_bodies(tl(bodies))
1.414 + end
1.415 + | format_body (Body_Pos(PLUS,_,_,_,x::y::xs,_,_),cent) =
1.416 + "\\rail@plus\n" ^ format_body(x, cent) ^
1.417 + "\\rail@nextplus{" ^ string_of_int(getystart(y)) ^ "}\n" ^
1.418 + format_body(y, "c") ^
1.419 + "\\rail@endplus\n"
1.420 + | format_body (Body_Pos(ANNOTE,text,_,_,_,_,_),cent) =
1.421 + "\\rail@annote[" ^ text ^ "]\n"
1.422 + | format_body (Body_Pos(IDENT,_,annot,Id(name,TERM),_,_,_),cent) =
1.423 + "\\rail@" ^ cent ^ "token{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
1.424 + | format_body (Body_Pos(IDENT,_,annot,Id(name,_),_,_,_),cent) =
1.425 + "\\rail@" ^ cent ^ "nont{" ^ name ^ "}" ^ "[" ^ annot ^ "]\n"
1.426 + | format_body (Body_Pos(CR,_,_,_,_,_,ynext),cent) =
1.427 + "\\rail@cr{" ^ string_of_int(ynext) ^ "}\n"
1.428 + | format_body (Body_Pos(STRING,text,annot,_,_,_,_),cent) =
1.429 + "\\rail@" ^ cent ^ "term{" ^ text ^ "}[" ^ annot ^ "]\n"
1.430 + | format_body _ =
1.431 + "\\rail@unknown\n";
1.432 +
1.433 +fun out_body (Id(name,_), body) =
1.434 + let val bodyPos as Body_Pos(_,_,_,_,_,_,ynext) = position_body(body,0)
1.435 + in
1.436 + "\\rail@begin{" ^ string_of_int(ynext) ^ "}{" ^ name ^ "}\n" ^
1.437 + format_body(bodyPos,"") ^
1.438 + "\\rail@end\n"
1.439 + end
1.440 + | out_body (Null_Id, body) = out_body (Id("", UNKNOWN), body);
1.441 +
1.442 +fun out_rule (Rule(id, body)) =
1.443 + if is_empty body then ""
1.444 + else out_body (id, body);
1.445 +
1.446 +fun out_rules ([]) = ""
1.447 + | out_rules (rule::rules) = out_rule rule ^ out_rules rules;
1.448 +
1.449 +val output_no_rules =
1.450 + "\\rail@begin{1}{}\n" ^
1.451 + "\\rail@setbox{\\bfseries ???}\n" ^
1.452 + "\\rail@oval\n" ^
1.453 + "\\rail@end\n";
1.454 +
1.455 +
1.456 +fun print (SOME rules) =
1.457 + "\\begin{railoutput}\n" ^
1.458 + out_rules rules ^
1.459 + "\\end{railoutput}\n"
1.460 + | print (NONE) =
1.461 + "\\begin{railoutput}\n" ^
1.462 + output_no_rules ^
1.463 + "\\end{railoutput}\n";
1.464 +
1.465 +fun process txt ctxt =
1.466 + lex txt ctxt
1.467 + |> parse
1.468 + |> print;
1.469 +
1.470 +val _ = ThyOutput.antiquotation "rail" (Scan.lift ( OuterParse.position Args.name ))
1.471 + (fn {context = ctxt,...} => fn txt => process txt ctxt);