# HG changeset patch
# User aspinall
# Date 1166546133 -3600
# Node ID f1790ca921e14ca22fcb0f5a9daf26cf64d009a7
# Parent  5a11263bd8cfeaac90b74b897dbe2b237d9f4746
Missing elements from doc_markup_elements

diff -r 5a11263bd8cf -r f1790ca921e1 src/Pure/ProofGeneral/pgip_markup.ML
--- 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"]