author | aspinall |
Mon, 22 Jan 2007 15:36:58 +0100 | |
changeset 22160 | 27cdecde8c2b |
parent 22101 | 6d13239d5f52 |
child 22374 | db0b80b8371c |
permissions | -rw-r--r-- |
21637 | 1 |
(* Title: Pure/ProofGeneral/parsing.ML |
2 |
ID: $Id$ |
|
3 |
Author: David Aspinall |
|
4 |
||
21867 | 5 |
Parsing Isabelle theory files to add PGIP markup. |
21637 | 6 |
*) |
7 |
||
8 |
signature PGIP_PARSER = |
|
9 |
sig |
|
21867 | 10 |
val pgip_parser: PgipMarkup.pgip_parser |
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
11 |
val init : unit -> unit (* clear state *) |
21637 | 12 |
end |
13 |
||
14 |
structure PgipParser : PGIP_PARSER = |
|
15 |
struct |
|
16 |
||
17 |
||
18 |
(** Parsing proof scripts without execution **) |
|
19 |
||
20 |
structure P = OuterParse; |
|
21 |
||
21867 | 22 |
structure D = PgipMarkup; |
23 |
||
21637 | 24 |
(* Notes. |
25 |
This is quite tricky, because 1) we need to put back whitespace which |
|
26 |
was removed during parsing so we can provide markup around commands; |
|
27 |
2) parsing is intertwined with execution in Isar so we have to repeat |
|
28 |
the parsing to extract interesting parts of commands. The trace of |
|
29 |
tokens parsed which is now recorded in each transition (added by |
|
30 |
Markus June '04) helps do this, but the mechanism is still a bad mess. |
|
31 |
||
32 |
If we had proper parse trees it would be easy, although having a |
|
21867 | 33 |
fixed type of trees might be hard with Isar's extensible parser. |
21637 | 34 |
|
35 |
Probably the best solution is to produce the meta-information at |
|
36 |
the same time as the parse, for each command, e.g. by recording a |
|
37 |
list of (name,objtype) pairs which record the bindings created by |
|
38 |
a command. This would require changing the interfaces in |
|
39 |
outer_syntax.ML (or providing new ones), |
|
40 |
||
41 |
datatype metainfo = Binding of string * string (* name, objtype *) |
|
42 |
||
43 |
val command_withmetainfo: string -> string -> string -> |
|
44 |
(token list -> |
|
45 |
((Toplevel.transition -> Toplevel.transition) * metainfo list) * |
|
46 |
token list) -> parser |
|
47 |
||
48 |
We'd also like to render terms as they appear in output, but this |
|
49 |
will be difficult because inner syntax is extensible and we don't |
|
50 |
have the correct syntax to hand when just doing outer parsing |
|
51 |
without execution. A reasonable approximation could |
|
52 |
perhaps be obtained by using the syntax of the current context. |
|
53 |
However, this would mean more mess trying to pick out terms, |
|
54 |
so at this stage a more serious change to the Isar functions |
|
55 |
seems necessary. |
|
56 |
*) |
|
57 |
||
58 |
local |
|
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
59 |
val keywords_classification_table = ref (NONE: string Symtab.table option) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
60 |
|
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
61 |
in |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
62 |
fun get_keywords_classification_table () = |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
63 |
case (!keywords_classification_table) of |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
64 |
SOME t => t |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
65 |
| NONE => (let |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
66 |
val tab = fold (fn (c, _, k, _) => Symtab.update (c, k)) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
67 |
(OuterSyntax.dest_parsers ()) Symtab.empty; |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
68 |
in (keywords_classification_table := SOME tab; tab) end) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
69 |
|
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
70 |
(* To allow dynamic extensions to language during interactive use |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
71 |
we need a hook in outer_syntax.ML to reset our table. But this is |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
72 |
pretty obscure; initialisation at startup should suffice. *) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
73 |
|
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
74 |
fun init () = (keywords_classification_table := NONE) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
75 |
end |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
76 |
|
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
77 |
|
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
78 |
local |
21637 | 79 |
|
21867 | 80 |
fun whitespace str = D.Whitespace { text=str } |
21637 | 81 |
|
82 |
(* an extra token is needed to terminate the command *) |
|
83 |
val sync = OuterSyntax.scan "\\<^sync>"; |
|
84 |
||
21867 | 85 |
fun nameparse elt objtyp nameP toks = |
86 |
(fst (nameP (toks@sync))) |
|
87 |
handle _ => (error ("Error occurred in name parser for " ^ elt ^ |
|
88 |
"(objtype: " ^ objtyp ^ ")"); |
|
89 |
"") |
|
21637 | 90 |
|
91 |
fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg) |
|
92 |
||
93 |
fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *) |
|
94 |
let |
|
95 |
val ((thyname,imports,files),_) = ThyHeader.args (toks@sync) |
|
96 |
in |
|
21867 | 97 |
[D.Opentheory { thyname=thyname, |
98 |
parentnames = imports, |
|
99 |
text = str }] |
|
21637 | 100 |
end |
101 |
||
102 |
fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases *) |
|
103 |
let |
|
104 |
(* NB: PGIP only deals with single name bindings at the moment; |
|
105 |
potentially we could markup grouped definitions several times but |
|
106 |
that might suggest the wrong structure to the editor? |
|
107 |
Better alternative would be to put naming closer around text, |
|
108 |
but to do that we'd be much better off modifying the real parser |
|
109 |
instead of reconstructing it here. *) |
|
110 |
||
111 |
val plain_items = (* no names, unimportant names, or too difficult *) |
|
112 |
["defaultsort","arities","judgement","finalconsts", |
|
113 |
"syntax", "nonterminals", "translations", |
|
114 |
"global", "local", "hide", |
|
115 |
"ML_setup", "setup", "method_setup", |
|
116 |
"parse_ast_translation", "parse_translation", "print_translation", |
|
117 |
"typed_print_translation", "print_ast_translation", "token_translation", |
|
118 |
"oracle", |
|
119 |
"declare"] |
|
120 |
||
21867 | 121 |
fun named_item nameP ty = |
122 |
[D.Theoryitem {text=str,name=SOME (nameparse "theoryitem" ty nameP toks),objtype=SOME ty}] |
|
123 |
val plain_item = |
|
124 |
[D.Theoryitem {text=str,name=NONE,objtype=NONE}] |
|
125 |
val doccomment = |
|
126 |
[D.Doccomment {text=str}] |
|
21637 | 127 |
|
128 |
val opt_overloaded = P.opt_keyword "overloaded"; |
|
129 |
||
130 |
val thmnameP = (* see isar_syn.ML/theoremsP *) |
|
131 |
let |
|
22101 | 132 |
val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1) |
133 |
val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x) |
|
21637 | 134 |
in |
135 |
theoremsP |
|
136 |
end |
|
137 |
in |
|
138 |
(* TODO: ideally we would like to render terms properly, just as they are |
|
139 |
in output. This implies using PGML for symbols and variables/atoms. |
|
140 |
BUT it's rather tricky without having the correct concrete syntax to hand, |
|
141 |
and even if we did, we'd have to mess around here a whole lot more first |
|
142 |
to pick out the terms from the syntax. *) |
|
143 |
||
144 |
if member (op =) plain_items name then plain_item |
|
145 |
else case name of |
|
21867 | 146 |
"text" => doccomment |
147 |
| "text_raw" => doccomment |
|
21637 | 148 |
| "typedecl" => named_item (P.type_args |-- P.name) "type" |
149 |
| "types" => named_item (P.type_args |-- P.name) "type" |
|
150 |
| "classes" => named_item P.name "class" |
|
151 |
| "classrel" => named_item P.name "class" |
|
152 |
| "consts" => named_item (P.const >> #1) "term" |
|
22101 | 153 |
| "axioms" => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem" |
154 |
| "defs" => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem" |
|
21637 | 155 |
| "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term" |
156 |
| "theorems" => named_item thmnameP "thmset" |
|
157 |
| "lemmas" => named_item thmnameP "thmset" |
|
158 |
| "oracle" => named_item P.name "oracle" |
|
159 |
| "locale" => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale" |
|
21867 | 160 |
| _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); |
161 |
plain_item) |
|
21637 | 162 |
end |
163 |
||
164 |
fun xmls_of_thy_goal (name,toks,str) = |
|
165 |
let |
|
166 |
(* see isar_syn.ML/gen_theorem *) |
|
22101 | 167 |
val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp); |
21637 | 168 |
val general_statement = |
22101 | 169 |
statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement); |
21637 | 170 |
|
171 |
val gen_theoremP = |
|
22101 | 172 |
P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --| |
173 |
Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) -- |
|
21637 | 174 |
general_statement >> (fn ((locale, a), (elems, concl)) => |
175 |
fst a) (* a : (bstring * Args.src list) *) |
|
176 |
||
22101 | 177 |
val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "") |
21867 | 178 |
val thmname = nameparse "opengoal" "theorem" nameP toks |
21637 | 179 |
in |
21867 | 180 |
[D.Opengoal {thmname=SOME thmname, text=str}, |
181 |
D.Openblock {metavarid=NONE,name=NONE,objtype=SOME "theorem-proof"}] |
|
21637 | 182 |
end |
183 |
||
21867 | 184 |
fun xmls_of_qed (name,str) = |
21637 | 185 |
let val qedmarkup = |
186 |
(case name of |
|
21867 | 187 |
"sorry" => D.Postponegoal {text=str} |
188 |
| "oops" => D.Giveupgoal {text=str} |
|
189 |
| "done" => D.Closegoal {text=str} |
|
190 |
| "by" => D.Closegoal {text=str} (* nested or toplevel *) |
|
191 |
| "qed" => D.Closegoal {text=str} (* nested or toplevel *) |
|
192 |
| "." => D.Closegoal {text=str} (* nested or toplevel *) |
|
193 |
| ".." => D.Closegoal {text=str} (* nested or toplevel *) |
|
21637 | 194 |
| other => (* default to closegoal: may be wrong for extns *) |
195 |
(parse_warning |
|
196 |
("Unrecognized qed command: " ^ quote other); |
|
21867 | 197 |
D.Closegoal {text=str})) |
198 |
in qedmarkup :: [D.Closeblock {}] end |
|
21637 | 199 |
|
200 |
fun xmls_of_kind kind (name,toks,str) = |
|
201 |
case kind of |
|
21867 | 202 |
"control" => [D.Badcmd {text=str}] |
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
203 |
| "diag" => [D.Spuriouscmd {text=str}] |
21637 | 204 |
(* theory/files *) |
205 |
| "theory-begin" => xmls_of_thy_begin (name,toks,str) |
|
206 |
| "theory-decl" => xmls_of_thy_decl (name,toks,str) |
|
21867 | 207 |
| "theory-heading" => [D.Doccomment {text=str}] |
208 |
| "theory-script" => [D.Theoryitem {name=NONE,objtype=NONE,text=str}] |
|
209 |
| "theory-end" => [D.Closetheory {text=str}] |
|
21637 | 210 |
(* proof control *) |
211 |
| "theory-goal" => xmls_of_thy_goal (name,toks,str) |
|
21867 | 212 |
| "proof-heading" => [D.Doccomment {text=str}] |
213 |
||
214 |
| "proof-goal" => (* nested proof: have, show, ... *) |
|
215 |
[D.Opengoal {text=str,thmname=NONE}, |
|
216 |
D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] |
|
217 |
||
218 |
| "proof-block" => [D.Proofstep {text=str}] |
|
219 |
| "proof-open" => [D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}, |
|
220 |
D.Proofstep {text=str} ] |
|
221 |
| "proof-close" => [D.Proofstep {text=str}, D.Closeblock {}] |
|
222 |
| "proof-script" => [D.Proofstep {text=str}] |
|
223 |
| "proof-chain" => [D.Proofstep {text=str}] |
|
224 |
| "proof-decl" => [D.Proofstep {text=str}] |
|
225 |
| "proof-asm" => [D.Proofstep {text=str}] |
|
226 |
| "proof-asm-goal" => (* nested proof: obtain, ... *) |
|
227 |
[D.Opengoal {text=str,thmname=NONE}, |
|
228 |
D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}] |
|
229 |
||
230 |
| "qed" => xmls_of_qed (name,str) |
|
231 |
| "qed-block" => xmls_of_qed (name,str) |
|
232 |
| "qed-global" => xmls_of_qed (name,str) |
|
233 |
| other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *) |
|
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
234 |
(parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other ^ |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
235 |
"(treated as spuriouscmd)"); |
21867 | 236 |
[D.Spuriouscmd {text=str}]) |
21637 | 237 |
in |
238 |
||
239 |
fun xmls_of_transition (name,str,toks) = |
|
240 |
let |
|
241 |
val classification = Symtab.lookup (get_keywords_classification_table ()) name |
|
242 |
in case classification of |
|
243 |
SOME k => (xmls_of_kind k (name,toks,str)) |
|
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
244 |
| NONE => (* an uncategorized keyword is treated as a theory item (maybe wrong) *) |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
245 |
(parse_warning ("Uncategorized command found: " ^ name ^ " -- using theoryitem"); |
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
246 |
[D.Theoryitem {name=NONE,objtype=NONE,text=str}]) |
21637 | 247 |
end |
248 |
||
22160 | 249 |
|
250 |
(* this would be a lot neater if we could match on toks! *) |
|
21637 | 251 |
fun markup_comment_whs [] = [] |
22160 | 252 |
| markup_comment_whs (toks as t::ts) = |
21637 | 253 |
let |
254 |
val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks |
|
255 |
in |
|
21902 | 256 |
if not (null prewhs) then |
21867 | 257 |
D.Whitespace {text=implode (map OuterLex.unparse prewhs)} |
21637 | 258 |
:: (markup_comment_whs rest) |
259 |
else |
|
21867 | 260 |
D.Comment {text=OuterLex.unparse t} :: |
21637 | 261 |
(markup_comment_whs ts) |
262 |
end |
|
263 |
||
264 |
fun xmls_pre_cmd [] = ([],[]) |
|
265 |
| xmls_pre_cmd toks = |
|
266 |
let |
|
267 |
(* an extra token is needed to terminate the command *) |
|
268 |
val sync = OuterSyntax.scan "\\<^sync>"; |
|
269 |
val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode |
|
270 |
val text_with_whs = |
|
271 |
((spaceP || Scan.succeed "") -- |
|
272 |
(P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^) |
|
273 |
-- (spaceP || Scan.succeed "") >> op^ |
|
274 |
val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync) |
|
21971
513e1d82640d
Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents:
21966
diff
changeset
|
275 |
(* NB: this collapses doccomment,(doccomment|whitespace)* to a single doccomment *) |
21637 | 276 |
val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1 |
277 |
val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2 |
|
278 |
in |
|
279 |
((markup_comment_whs prewhs) @ |
|
280 |
(if (length rest2 = length rest1) then [] |
|
21867 | 281 |
else |
282 |
[D.Doccomment |
|
283 |
{text= implode |
|
284 |
(map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))}] |
|
285 |
@ |
|
286 |
(markup_comment_whs postwhs)), |
|
287 |
Library.take (length rest3 - 1,rest3)) |
|
21637 | 288 |
end |
289 |
||
290 |
fun xmls_of_impropers toks = |
|
291 |
let |
|
292 |
val (xmls,rest) = xmls_pre_cmd toks |
|
21867 | 293 |
val unparsed = |
294 |
case rest of [] => [] |
|
295 |
| _ => [D.Unparseable |
|
296 |
{text= implode (map OuterLex.unparse rest)}] |
|
21637 | 297 |
in |
21867 | 298 |
xmls @ unparsed |
21637 | 299 |
end |
300 |
||
301 |
end |
|
302 |
||
303 |
||
304 |
local |
|
305 |
(* we have to weave together the whitespace/comments with proper tokens |
|
306 |
to reconstruct the input. *) |
|
307 |
(* TODO: see if duplicating isar_output/parse_thy can help here *) |
|
308 |
||
309 |
fun match_tokens ([],us,vs) = (rev vs,us) (* used, unused *) |
|
21902 | 310 |
| match_tokens (t::ts, w::ws, vs) = |
21966 | 311 |
if (t: OuterLex.token) = w (* FIXME !? *) |
21902 | 312 |
then match_tokens (ts, ws, w::vs) |
313 |
else match_tokens (t::ts, ws, w::vs) |
|
21637 | 314 |
| match_tokens _ = error ("match_tokens: mismatched input parse") |
315 |
in |
|
21867 | 316 |
fun pgip_parser str = |
21637 | 317 |
let |
318 |
(* parsing: See outer_syntax.ML/toplevel_source *) |
|
319 |
fun parse_loop ([],[],xmls) = xmls |
|
320 |
| parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks) |
|
321 |
| parse_loop ((nm,toks,_)::trs,itoks,xmls) = |
|
322 |
let |
|
323 |
(* first proper token after whitespace/litcomment/whitespace is command *) |
|
324 |
val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks |
|
22160 | 325 |
val (cmdtok,itoks') = |
326 |
case cmditoks' of x::xs => (x,xs) |
|
327 |
| _ => error("proof_general/parse_loop impossible") |
|
21637 | 328 |
val (utoks,itoks'') = match_tokens (toks,itoks',[]) |
329 |
(* FIXME: should take trailing [w/s+] semicolon too in utoks *) |
|
330 |
||
331 |
val str = implode (map OuterLex.unparse (cmdtok::utoks)) |
|
332 |
||
333 |
val xmls_tr = xmls_of_transition (nm,str,toks) |
|
334 |
in |
|
335 |
parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr) |
|
336 |
end |
|
337 |
in |
|
338 |
(let val toks = OuterSyntax.scan str |
|
339 |
in |
|
340 |
parse_loop (OuterSyntax.read toks, toks, []) |
|
341 |
end) |
|
21867 | 342 |
handle _ => [D.Unparseable {text=str}] |
21637 | 343 |
end |
344 |
end |
|
345 |
||
346 |
end |