--- a/src/Pure/ProofGeneral/pgip_markup.ML Tue Dec 19 16:58:30 2006 +0100
+++ b/src/Pure/ProofGeneral/pgip_markup.ML Tue Dec 19 17:35:33 2006 +0100
@@ -178,21 +178,25 @@
val doc_markup_elements =
["openblock",
"closeblock",
+ "opentheory",
+ "theoryitem",
+ "closetheory",
"opengoal",
"proofstep",
"closegoal",
+ "giveupgoal",
+ "postponegoal",
"comment",
"doccomment",
"whitespace",
- "litcomment",
"spuriouscmd",
"badcmd",
- "opentheory",
- "theoryitem",
- "closetheory",
+ (* the prover shouldn't really receive the next ones,
+ but we include them here so that they are harmlessly
+ ignored. *)
+ "unparseable",
"metainfo",
- (* the prover should never receive the next three,
- but we include them here so that they are ignored. *)
+ (* Broker document format *)
"litcomment",
"showcode",
"setformat"]