# HG changeset patch
# User aspinall
# Date 1171729373 -3600
# Node ID 050ceb64920711d09985ad1147af7bb992184a89
# Parent  6c4204df68636ede2a2d465b10bdb77e71a8751d
<idvalue>: add name attribute to allow unsolicited updates.

diff -r 6c4204df6863 -r 050ceb649207 src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Sat Feb 17 17:19:59 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Sat Feb 17 17:22:53 2007 +0100
@@ -43,8 +43,9 @@
 			       name: PgipTypes.objname option,
 			       idtables: PgipTypes.idtable list,
 			       fileurls : PgipTypes.pgipurl list }
-    | Idvalue             of { name: PgipTypes.objname, 
+    | Idvalue             of { thyname: PgipTypes.objname option,
 			       objtype: PgipTypes.objtype, 
+			       name: PgipTypes.objname, 
 			       text: XML.content }
     | Informguise         of { file : PgipTypes.pgipurl option,  
                                theory: PgipTypes.objname option, 
@@ -90,8 +91,9 @@
        | Addids              of { idtables: PgipTypes.idtable list }
        | Hasprefs            of { prefcategory: string option, prefs: preference list }
        | Prefval             of { name: string, value: string }
-       | Idvalue             of { name: PgipTypes.objname, 
+       | Idvalue             of { thyname: PgipTypes.objname option,
 				  objtype: PgipTypes.objtype, 
+				  name: PgipTypes.objname, 
 				  text: XML.content }
        | Setrefs             of { url: PgipTypes.pgipurl option,
 				  thyname: PgipTypes.objname option,
@@ -287,11 +289,16 @@
 
 fun idvalue (Idvalue vs) =
     let 
+	val objtype_attrs = attrs_of_objtype (#objtype vs)
+	val thyname = #thyname vs
         val name = #name vs
-	val objtype_attrs = attrs_of_objtype (#objtype vs)
         val text = #text vs
     in
-        XML.Elem("idvalue", attr "name" name @ objtype_attrs, text)
+        XML.Elem("idvalue", 
+		 objtype_attrs @
+		 (opt_attr "thyname" thyname) @
+		 (attr "name" name),
+		 text)
     end
 
 fun informguise (Informguise vs) =