# HG changeset patch
# User aspinall
# Date 1169476628 -3600
# Node ID b2117f4f2d3919d66198294b3e1dc032b0d2480a
# Parent  27cdecde8c2b5f2929f05d93d272c91896953b43
Add askrefs, setrefs, error_with_pos

diff -r 27cdecde8c2b -r b2117f4f2d39 src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Mon Jan 22 15:36:58 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Mon Jan 22 15:37:08 2007 +0100
@@ -35,6 +35,10 @@
     | Askids         of { url: PgipTypes.pgipurl option,
 			  thyname: PgipTypes.objname option,
 			  objtype: PgipTypes.objtype option }
+    | Askrefs        of { url: PgipTypes.pgipurl option,
+			  thyname: PgipTypes.objname option,
+			  objtype: PgipTypes.objtype option,
+			  name: PgipTypes.objname option }
     | Showid         of { thyname: PgipTypes.objname option, 
 			  objtype: PgipTypes.objtype, 
 			  name: PgipTypes.objname }
@@ -99,6 +103,10 @@
        | Askids         of { url: PgipTypes.pgipurl option,
 			     thyname: PgipTypes.objname option,
 			     objtype: PgipTypes.objtype option }
+       | Askrefs        of { url: PgipTypes.pgipurl option,
+			     thyname: PgipTypes.objname option,
+			     objtype: PgipTypes.objtype option,
+			     name: PgipTypes.objname option }
        | Showid         of { thyname: PgipTypes.objname option, 
 			     objtype: PgipTypes.objtype, 
 			     name: PgipTypes.objname }
@@ -191,6 +199,10 @@
    | "askids"         => Askids { url = pgipurl_attro attrs,
 				  thyname = thyname_attro attrs, 
 				  objtype = objtype_attro attrs }
+   | "askrefs"        => Askrefs { url = pgipurl_attro attrs,
+				   thyname = thyname_attro attrs, 
+				   objtype = objtype_attro attrs,
+				   name = name_attro attrs }
    | "showid"         => Showid { thyname = thyname_attro attrs,
 				  objtype = objtype_of_attrs attrs,
 				  name = name_attr attrs }
diff -r 27cdecde8c2b -r b2117f4f2d39 src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Mon Jan 22 15:36:58 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Mon Jan 22 15:37:08 2007 +0100
@@ -37,6 +37,12 @@
     | Hasprefs            of { prefcategory: string option, 
                                prefs: PgipTypes.preference list }
     | Prefval             of { name: string, value: string }
+    | Setrefs             of { url: PgipTypes.pgipurl option,
+			       thyname: PgipTypes.objname option,
+			       objtype: PgipTypes.objtype option,
+			       name: PgipTypes.objname option,
+			       idtables: PgipTypes.idtable list,
+			       fileurls : PgipTypes.pgipurl list }
     | Idvalue             of { name: PgipTypes.objname, 
 			       objtype: PgipTypes.objtype, 
 			       text: XML.content }
@@ -87,6 +93,12 @@
        | Idvalue             of { name: PgipTypes.objname, 
 				  objtype: PgipTypes.objtype, 
 				  text: XML.content }
+       | Setrefs             of { url: PgipTypes.pgipurl option,
+				  thyname: PgipTypes.objname option,
+				  objtype: PgipTypes.objtype option,
+				  name: PgipTypes.objname option,
+				  idtables: PgipTypes.idtable list,
+				  fileurls : PgipTypes.pgipurl list }
        | Informguise         of { file : PgipTypes.pgipurl option,  
 				  theory: PgipTypes.objname option, 
 				  theorem: PgipTypes.objname option, 
@@ -224,6 +236,25 @@
         XML.Elem ("setids",[],map idtable_to_xml idtables)
     end
 
+fun setrefs (Setrefs vs) =
+    let
+	val url = #url vs
+	val thyname = #thyname vs
+	val objtype = #objtype vs
+	val name = #name vs
+        val idtables = #idtables vs
+        val fileurls = #fileurls vs
+	fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
+    in
+        XML.Elem ("setrefs",
+		  (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ 
+		  (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
+		  (opt_attr "thyname" thyname) @
+		  (opt_attr "name" name),
+		  (map idtable_to_xml idtables) @ 
+		  (map fileurl_to_xml fileurls))
+    end
+
 fun addids (Addids vs) =
     let
         val idtables = #idtables vs
@@ -356,6 +387,7 @@
   | Lexicalstructure _      => lexicalstructure pgipoutput
   | Proverinfo _            => proverinfo pgipoutput
   | Setids _                => setids pgipoutput
+  | Setrefs _               => setrefs pgipoutput
   | Addids _                => addids pgipoutput
   | Delids _                => delids pgipoutput
   | Hasprefs _              => hasprefs pgipoutput