# HG changeset patch
# User wenzelm
# Date 1207240959 -7200
# Node ID 14b268974c4b3c7f4c56355b7139d90e3e1c0249
# Parent  173d548ce9d21a7d5b1e14880f5a1e7f6df3ad94
XML.string_of, XML.parse;

diff -r 173d548ce9d2 -r 14b268974c4b src/Pure/ProofGeneral/pgip_tests.ML
--- a/src/Pure/ProofGeneral/pgip_tests.ML	Thu Apr 03 18:42:38 2008 +0200
+++ b/src/Pure/ProofGeneral/pgip_tests.ML	Thu Apr 03 18:42:39 2008 +0200
@@ -14,25 +14,23 @@
     else error("PGIP test: expected these two values to be equal:\n" ^
 	       (toS a) ^"\n and: \n" ^ (toS b))
 
-val asseqx = asseq_p XML.string_of_tree
+val asseqx = asseq_p XML.string_of
 val asseqs = asseq_p I
 val asseqb = asseq_p (fn b=>if b then "true" else "false")
 
-val p = XML.tree_of_string (* parse *)
-
 open PgipTypes;
 in
 
-val _ = asseqx (pgiptype_to_xml Pgipnull) (p "<pgipnull/>");
-val _ = asseqx (pgiptype_to_xml Pgipbool) (p "<pgipbool/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (p "<pgipint/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (p "<pgipint min='5' max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (p "<pgipint max='7'/>");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (p "<pgipint min='-5'/>");
-val _ = asseqx (pgiptype_to_xml Pgipstring) (p "<pgipstring/>");
-val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (p "<pgipconst name='radio1'/>");
+val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
+val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
+val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
+val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (XML.parse "<pgipconst name='radio1'/>");
 val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
-       (p "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
+       (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
 
 val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
 val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
@@ -54,16 +52,14 @@
 
 val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
 		 default=SOME "true", pgiptype=Pgipbool})
-       (p "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
+       (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
 end
 
 
 (** pgip_input.ML **)
 local
 
-val p = XML.tree_of_string (* parse *)
-
-fun e str = case p str of 
+fun e str = case XML.parse str of 
 		(XML.Elem args) => args
 	      | _ => error("Expected to get an XML Element")
 
diff -r 173d548ce9d2 -r 14b268974c4b src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 18:42:38 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 18:42:39 2008 +0200
@@ -141,16 +141,16 @@
 fun matching_pgip_id id = (id = !pgip_id)
 
 val output_xml_fn = ref Output.writeln_default
-fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
+fun output_xml s = (!output_xml_fn) (XML.string_of s);  (* TODO: string buffer *)
 
 val output_pgips =
-  XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
+  XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
 
 val output_pgmlterm = 
-  XML.string_of_tree o Pgml.pgmlterm_to_xml;
+  XML.string_of o Pgml.pgmlterm_to_xml;
 
 val output_pgmltext = 
-  XML.string_of_tree o Pgml.pgml_to_xml;
+  XML.string_of o Pgml.pgml_to_xml;
 
 
 fun issue_pgip_rawtext str =
@@ -1031,7 +1031,7 @@
         xml as (XML.Elem elem) =>
         (case Pgip.input elem of
              NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
-                              (XML.string_of_tree xml))
+                              (XML.string_of xml))
            | SOME inp => (process_input inp)) (* errors later; packet discarded *)
       | XML.Text t => ignored_text_warning t
       | XML.Output t => ignored_text_warning t
@@ -1067,12 +1067,12 @@
         | _ => raise PGIP "Invalid PGIP packet received")
      handle PGIP msg =>
             (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
-                               (XML.string_of_tree xml));
+                               (XML.string_of xml));
              true))
 
 (* External input *)
 
-val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
+val process_pgip_plain = K () o process_pgip_tree o XML.parse
 
 (* PGIP loop: process PGIP input only *)
 
@@ -1115,7 +1115,7 @@
 in
   (* TODO: add socket interface *)
 
-  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
+  val xmlP = XML.parse_comment_whspc |-- XML.parse_elem >> single
 
   val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)