1.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Thu Apr 03 18:42:38 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Thu Apr 03 18:42:39 2008 +0200
     1.3 @@ -14,25 +14,23 @@
     1.4      else error("PGIP test: expected these two values to be equal:\n" ^
     1.5  	       (toS a) ^"\n and: \n" ^ (toS b))
     1.6  
     1.7 -val asseqx = asseq_p XML.string_of_tree
     1.8 +val asseqx = asseq_p XML.string_of
     1.9  val asseqs = asseq_p I
    1.10  val asseqb = asseq_p (fn b=>if b then "true" else "false")
    1.11  
    1.12 -val p = XML.tree_of_string (* parse *)
    1.13 -
    1.14  open PgipTypes;
    1.15  in
    1.16  
    1.17 -val _ = asseqx (pgiptype_to_xml Pgipnull) (p "<pgipnull/>");
    1.18 -val _ = asseqx (pgiptype_to_xml Pgipbool) (p "<pgipbool/>");
    1.19 -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (p "<pgipint/>");
    1.20 -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (p "<pgipint min='5' max='7'/>");
    1.21 -val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (p "<pgipint max='7'/>");
    1.22 -val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (p "<pgipint min='-5'/>");
    1.23 -val _ = asseqx (pgiptype_to_xml Pgipstring) (p "<pgipstring/>");
    1.24 -val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (p "<pgipconst name='radio1'/>");
    1.25 +val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "<pgipnull/>");
    1.26 +val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "<pgipbool/>");
    1.27 +val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "<pgipint/>");
    1.28 +val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "<pgipint min='5' max='7'/>");
    1.29 +val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "<pgipint max='7'/>");
    1.30 +val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "<pgipint min='-5'/>");
    1.31 +val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "<pgipstring/>");
    1.32 +val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1"))  (XML.parse "<pgipconst name='radio1'/>");
    1.33  val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
    1.34 -       (p "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
    1.35 +       (XML.parse "<pgipchoice><pgipbool descr='the best choice'/></pgipchoice>");
    1.36  
    1.37  val _ = asseqs (pgval_to_string (read_pgval Pgipbool "true")) "true";
    1.38  val _ = asseqs (pgval_to_string (read_pgval Pgipbool "false")) "false";
    1.39 @@ -54,16 +52,14 @@
    1.40  
    1.41  val _ = asseqx (haspref {name="provewithgusto",descr=SOME "use energetic proofs",
    1.42  		 default=SOME "true", pgiptype=Pgipbool})
    1.43 -       (p "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
    1.44 +       (XML.parse "<haspref name='provewithgusto' descr='use energetic proofs' default='true'><pgipbool/></haspref>");
    1.45  end
    1.46  
    1.47  
    1.48  (** pgip_input.ML **)
    1.49  local
    1.50  
    1.51 -val p = XML.tree_of_string (* parse *)
    1.52 -
    1.53 -fun e str = case p str of 
    1.54 +fun e str = case XML.parse str of 
    1.55  		(XML.Elem args) => args
    1.56  	      | _ => error("Expected to get an XML Element")
    1.57  

     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 18:42:38 2008 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Apr 03 18:42:39 2008 +0200
     2.3 @@ -141,16 +141,16 @@
     2.4  fun matching_pgip_id id = (id = !pgip_id)
     2.5  
     2.6  val output_xml_fn = ref Output.writeln_default
     2.7 -fun output_xml s = (!output_xml_fn) (XML.string_of_tree s);  (* TODO: string buffer *)
     2.8 +fun output_xml s = (!output_xml_fn) (XML.string_of s);  (* TODO: string buffer *)
     2.9  
    2.10  val output_pgips =
    2.11 -  XML.string_of_tree o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    2.12 +  XML.string_of o PgipOutput.output o assemble_pgips o map PgipOutput.output;
    2.13  
    2.14  val output_pgmlterm = 
    2.15 -  XML.string_of_tree o Pgml.pgmlterm_to_xml;
    2.16 +  XML.string_of o Pgml.pgmlterm_to_xml;
    2.17  
    2.18  val output_pgmltext = 
    2.19 -  XML.string_of_tree o Pgml.pgml_to_xml;
    2.20 +  XML.string_of o Pgml.pgml_to_xml;
    2.21  
    2.22  
    2.23  fun issue_pgip_rawtext str =
    2.24 @@ -1031,7 +1031,7 @@
    2.25          xml as (XML.Elem elem) =>
    2.26          (case Pgip.input elem of
    2.27               NONE => warning ("Unrecognized PGIP command, ignored: \n" ^
    2.28 -                              (XML.string_of_tree xml))
    2.29 +                              (XML.string_of xml))
    2.30             | SOME inp => (process_input inp)) (* errors later; packet discarded *)
    2.31        | XML.Text t => ignored_text_warning t
    2.32        | XML.Output t => ignored_text_warning t
    2.33 @@ -1067,12 +1067,12 @@
    2.34          | _ => raise PGIP "Invalid PGIP packet received")
    2.35       handle PGIP msg =>
    2.36              (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^
    2.37 -                               (XML.string_of_tree xml));
    2.38 +                               (XML.string_of xml));
    2.39               true))
    2.40  
    2.41  (* External input *)
    2.42  
    2.43 -val process_pgip_plain = K () o process_pgip_tree o XML.tree_of_string
    2.44 +val process_pgip_plain = K () o process_pgip_tree o XML.parse
    2.45  
    2.46  (* PGIP loop: process PGIP input only *)
    2.47  
    2.48 @@ -1115,7 +1115,7 @@
    2.49  in
    2.50    (* TODO: add socket interface *)
    2.51  
    2.52 -  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
    2.53 +  val xmlP = XML.parse_comment_whspc |-- XML.parse_elem >> single
    2.54  
    2.55    val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP NONE Source.tty)
    2.56