# HG changeset patch
# User aspinall
# Date 1172921990 -3600
# Node ID 790935f7c1abdf84ad8ec3d00ca1803568a3bdbf
# Parent  12892a6677c6ef644d48abdbe4bdd6745451d4d9
Add more attributes to openblock.  Change theory item objtype field to proper objtype.

diff -r 12892a6677c6 -r 790935f7c1ab src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Sat Mar 03 12:38:36 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Sat Mar 03 12:39:50 2007 +0100
@@ -9,10 +9,10 @@
 sig
   (* Generic markup on sequential, non-overlapping pieces of proof text *)
   datatype pgipdoc = 
-    Openblock     of { metavarid: string option, name: string option, objtype: string option }
+    Openblock     of { metavarid: string option, name: string option, objtype: PgipTypes.objtype option }
   | Closeblock    of { }
   | Opentheory    of { thyname: string, parentnames: string list , text: string}
-  | Theoryitem    of { name: string option, objtype: string option, text: string }
+  | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
   | Closetheory   of { text: string }
   | Opengoal	  of { thmname: string option, text: string }
   | Proofstep     of { text: string }
@@ -46,10 +46,10 @@
 
 (* PGIP 3 idea: replace opentheory, opengoal, etc. by just openblock with corresponding objtype? *)
   datatype pgipdoc = 
-    Openblock     of { metavarid: string option, name: string option, objtype: string option }
+    Openblock     of { metavarid: string option, name: string option, objtype: PgipTypes.objtype option }
   | Closeblock    of { }
   | Opentheory    of { thyname: string, parentnames: string list, text: string}
-  | Theoryitem    of { name: string option, objtype: string option, text: string }
+  | Theoryitem    of { name: string option, objtype: PgipTypes.objtype option, text: string }
   | Closetheory   of { text: string }
   | Opengoal	  of { thmname: string option, text: string }
   | Proofstep     of { text: string }
@@ -74,7 +74,10 @@
        case docelt of
 
 	   Openblock vs  => 
-	   XML.Elem("openblock", opt_attr "metavarid" (#metavarid vs), [])
+	   XML.Elem("openblock", opt_attr "name" (#metavarid vs) @
+				 opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs) @
+				 opt_attr "metavarid" (#metavarid vs),
+		    [])
 	   
 	 | Closeblock vs => 
 	   XML.Elem("closeblock", [], [])
@@ -91,7 +94,7 @@
 	 | Theoryitem vs => 
 	   XML.Elem("theoryitem", 
 		    opt_attr "name" (#name vs) @
-		    opt_attr "objtype" (#objtype vs),
+		    opt_attr_map PgipTypes.name_of_objtype "objtype" (#objtype vs),
 		    [XML.Text (#text vs)])
 	   
 	 | Closetheory vs =>