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