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 "");
-val _ = asseqx (pgiptype_to_xml Pgipbool) (p "");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (p "");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (p "");
-val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (p "");
-val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (p "");
-val _ = asseqx (pgiptype_to_xml Pgipstring) (p "");
-val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (p "");
+val _ = asseqx (pgiptype_to_xml Pgipnull) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml Pgipbool) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,NONE))) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME 5,SOME 7))) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml (Pgipint (NONE,SOME 7))) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml (Pgipint (SOME ~5,NONE))) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml Pgipstring) (XML.parse "");
+val _ = asseqx (pgiptype_to_xml (Pgipconst "radio1")) (XML.parse "");
val _ = asseqx (pgiptype_to_xml (Pgipchoice [Pgipdtype (SOME "the best choice",Pgipbool)]))
- (p "");
+ (XML.parse "");
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 "");
+ (XML.parse "");
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")