equal
deleted
inserted
replaced
176 |
176 |
177 (* Names of all PGIP document markup elements *) |
177 (* Names of all PGIP document markup elements *) |
178 val doc_markup_elements = |
178 val doc_markup_elements = |
179 ["openblock", |
179 ["openblock", |
180 "closeblock", |
180 "closeblock", |
|
181 "opentheory", |
|
182 "theoryitem", |
|
183 "closetheory", |
181 "opengoal", |
184 "opengoal", |
182 "proofstep", |
185 "proofstep", |
183 "closegoal", |
186 "closegoal", |
|
187 "giveupgoal", |
|
188 "postponegoal", |
184 "comment", |
189 "comment", |
185 "doccomment", |
190 "doccomment", |
186 "whitespace", |
191 "whitespace", |
187 "litcomment", |
|
188 "spuriouscmd", |
192 "spuriouscmd", |
189 "badcmd", |
193 "badcmd", |
190 "opentheory", |
194 (* the prover shouldn't really receive the next ones, |
191 "theoryitem", |
195 but we include them here so that they are harmlessly |
192 "closetheory", |
196 ignored. *) |
|
197 "unparseable", |
193 "metainfo", |
198 "metainfo", |
194 (* the prover should never receive the next three, |
199 (* Broker document format *) |
195 but we include them here so that they are ignored. *) |
|
196 "litcomment", |
200 "litcomment", |
197 "showcode", |
201 "showcode", |
198 "setformat"] |
202 "setformat"] |
199 |
203 |
200 (* non-document/empty text, must be ignored *) |
204 (* non-document/empty text, must be ignored *) |