# HG changeset patch
# User wenzelm
# Date 1207250619 -7200
# Node ID 41bbcaf3e4810061f5dc12a969962d090c57f926
# Parent  1112375f6a692c6166818eabb06e3633b0fcda66
further cleanup of XML signature;

diff -r 1112375f6a69 -r 41bbcaf3e481 src/Pure/ProofGeneral/pgip_input.ML
--- a/src/Pure/ProofGeneral/pgip_input.ML	Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_input.ML	Thu Apr 03 21:23:39 2008 +0200
@@ -63,7 +63,7 @@
     (* unofficial escape command for debugging *)
     | Quitpgip       of { }
 
-    val input           : XML.element -> pgipinput option        (* raises PGIP *)
+    val input: string * XML.attributes * XML.tree list -> pgipinput option  (* raises PGIP *)
 end
 
 structure PgipInput : PGIPINPUT = 
diff -r 1112375f6a69 -r 41bbcaf3e481 src/Pure/ProofGeneral/pgip_markup.ML
--- a/src/Pure/ProofGeneral/pgip_markup.ML	Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_markup.ML	Thu Apr 03 21:23:39 2008 +0200
@@ -28,14 +28,14 @@
   | Unparseable   of { text: string }
   | Metainfo      of { name: string option, text: string }
   (* Last three for PGIP literate markup only: *)
-  | Litcomment    of { format: string option, content: XML.content }
+  | Litcomment    of { format: string option, content: XML.tree list }
   | Showcode      of { show: bool }
   | Setformat     of { format: string }
 
   type pgipdocument = pgipdoc list
   type pgip_parser  = string -> pgipdocument       (* system must provide a parser P *)
   val unparse_doc : pgipdocument -> string list    (* s.t. unparse (P x) = x         *)
-  val output_doc : pgipdocument -> XML.content
+  val output_doc : pgipdocument -> XML.tree list
   val doc_markup_elements : string list            (* used in pgip_input *)
   val doc_markup_elements_ignored : string list    (* used in pgip_input *)
 end
@@ -65,7 +65,7 @@
   | Badcmd        of { text: string }
   | Unparseable   of { text: string }
   | Metainfo      of { name: string option, text: string }
-  | Litcomment    of { format: string option, content: XML.content }
+  | Litcomment    of { format: string option, content: XML.tree list }
   | Showcode      of { show: bool }
   | Setformat     of { format: string }
 
diff -r 1112375f6a69 -r 41bbcaf3e481 src/Pure/ProofGeneral/pgip_output.ML
--- a/src/Pure/ProofGeneral/pgip_output.ML	Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML	Thu Apr 03 21:23:39 2008 +0200
@@ -9,16 +9,16 @@
 sig
     (* These are the PGIP messages which the prover emits. *) 
     datatype pgipoutput = 
-      Normalresponse      of { content: XML.content }
+      Normalresponse      of { content: XML.tree list }
     | Errorresponse       of { fatality: PgipTypes.fatality, 
                                location: PgipTypes.location option, 
-                               content: XML.content }
+                               content: XML.tree list }
     | Informfileloaded    of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileoutdated  of { url: PgipTypes.pgipurl, completed: bool }
     | Informfileretracted of { url: PgipTypes.pgipurl, completed: bool }
     | Metainforesponse    of { attrs: XML.attributes, 
-                               content: XML.content }
-    | Lexicalstructure    of { content: XML.content }
+                               content: XML.tree list }
+    | Lexicalstructure    of { content: XML.tree list }
     | Proverinfo          of { name: string, 
                                version: string, 
                                instance: string,
@@ -40,13 +40,13 @@
     | Idvalue             of { thyname: PgipTypes.objname option,
 			       objtype: PgipTypes.objtype, 
 			       name: PgipTypes.objname, 
-			       text: XML.content }
+			       text: XML.tree list }
     | Informguise         of { file : PgipTypes.pgipurl option,  
                                theory: PgipTypes.objname option, 
                                theorem: PgipTypes.objname option, 
                                proofpos: int option }
     | Parseresult         of { attrs: XML.attributes, doc:PgipMarkup.pgipdocument, 
-			       errs: XML.content } (* errs to become PGML *)
+			       errs: XML.tree list } (* errs to become PGML *)
     | Usespgip            of { version: string, 
                                pgipelems: (string * bool * string list) list }
     | Usespgml            of { version: string }
@@ -56,7 +56,7 @@
                                destid: string option,
                                refid: string option,
                                refseq: int option,
-                               content: XML.content }
+                               content: XML.tree list }
     | Ready               of { }
 
     val output : pgipoutput -> XML.tree                                  
@@ -67,15 +67,15 @@
 open PgipTypes
 
 datatype pgipoutput = 
-	 Normalresponse      of { content: XML.content }
+	 Normalresponse      of { content: XML.tree list }
        | Errorresponse       of { fatality: fatality, 
                                   location: location option, 
-				  content: XML.content }
+				  content: XML.tree list }
        | Informfileloaded    of { url: Path.T, completed: bool }
        | Informfileoutdated  of { url: Path.T, completed: bool }
        | Informfileretracted of { url: Path.T, completed: bool }
-       | Metainforesponse    of { attrs: XML.attributes, content: XML.content }
-       | Lexicalstructure    of { content: XML.content }
+       | Metainforesponse    of { attrs: XML.attributes, content: XML.tree list }
+       | Lexicalstructure    of { content: XML.tree list }
        | Proverinfo          of { name: string, version: string, instance: string,
                                   descr: string, url: Url.T, filenameextns: string }
        | Setids              of { idtables: PgipTypes.idtable list  }
@@ -86,7 +86,7 @@
        | Idvalue             of { thyname: PgipTypes.objname option,
 				  objtype: PgipTypes.objtype, 
 				  name: PgipTypes.objname, 
-				  text: XML.content }
+				  text: XML.tree list }
        | Setrefs             of { url: PgipTypes.pgipurl option,
 				  thyname: PgipTypes.objname option,
 				  objtype: PgipTypes.objtype option,
@@ -98,7 +98,7 @@
 				  theorem: PgipTypes.objname option, 
 				  proofpos: int option }
        | Parseresult         of { attrs: XML.attributes, doc: PgipMarkup.pgipdocument,
-				  errs: XML.content } (* errs to become PGML *)
+				  errs: XML.tree list } (* errs to become PGML *)
        | Usespgip            of { version: string, 
                                   pgipelems: (string * bool * string list) list }
        | Usespgml            of { version: string }
@@ -108,7 +108,7 @@
                                   destid: string option,
                                   refid: string option,
                                   refseq: int option,
-                                  content: XML.content }
+                                  content: XML.tree list }
        | Ready               of { }
 
 
diff -r 1112375f6a69 -r 41bbcaf3e481 src/Pure/ProofGeneral/pgml.ML
--- a/src/Pure/ProofGeneral/pgml.ML	Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML	Thu Apr 03 21:23:39 2008 +0200
@@ -33,7 +33,7 @@
 			  xref: PgipTypes.pgipurl option,
 			  content: pgmlterm list }
 	   | Alt of { kind: string option, content: pgmlterm list }
-	   | Embed of XML.content
+	   | Embed of XML.tree list
 	   | Raw of XML.tree
 
     datatype pgml = 
@@ -77,7 +77,7 @@
 			  xref: PgipTypes.pgipurl option,
 			  content: pgmlterm list }
 	   | Alt of { kind: string option, content: pgmlterm list }
-	   | Embed of XML.content
+	   | Embed of XML.tree list
 	   | Raw of XML.tree
 
 		       
diff -r 1112375f6a69 -r 41bbcaf3e481 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 21:23:38 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 21:23:39 2008 +0200
@@ -1115,7 +1115,7 @@
 in
   (* TODO: add socket interface *)
 
-  val xmlP = XML.parse_comment_whspc |-- XML.parse_elem >> single
+  val xmlP = XML.parse_comment_whspc |-- XML.parse_element >> single
 
   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)