# HG changeset patch
# User wenzelm
# Date 1284988131 -7200
# Node ID ccb223a4d49c8404fb79eabc03bbe11ebc416528
# Parent  386576a416ea3561383afe476d36e88f6decbdd7
added XML.content_of convenience -- cover XML.body, which is the general situation;

diff -r 386576a416ea -r ccb223a4d49c src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -363,11 +363,8 @@
     (map (fn (mtd_name, (outcome, timing)) => mtd_name ^ ": " ^ string_of_outcome outcome) results) ^
   "\n"
 
-(* XML.tree -> string *)
-fun plain_string_from_xml_tree t =
-  Buffer.empty |> XML.add_content t |> Buffer.content
 (* string -> string *)
-val unyxml = plain_string_from_xml_tree o YXML.parse
+val unyxml = XML.content_of o YXML.parse_body
 
 fun string_of_mutant_subentry' thy thm_name (t, results) =
   let
diff -r 386576a416ea -r ccb223a4d49c src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -70,9 +70,7 @@
 fun nat_subscript n =
   n |> string_of_int |> print_mode_active Symbol.xsymbolsN ? subscript
 
-fun plain_string_from_xml_tree t =
-  Buffer.empty |> XML.add_content t |> Buffer.content
-val unyxml = plain_string_from_xml_tree o YXML.parse
+val unyxml = XML.content_of o YXML.parse_body
 
 val is_long_identifier = forall Syntax.is_identifier o space_explode "."
 fun maybe_quote y =
diff -r 386576a416ea -r ccb223a4d49c src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/Pure/General/xml.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -12,6 +12,7 @@
     | Text of string
   type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
+  val content_of: body -> string
   val header: string
   val text: string -> string
   val element: string -> attributes -> string list -> string
@@ -41,6 +42,8 @@
 fun add_content (Elem (_, ts)) = fold add_content ts
   | add_content (Text s) = Buffer.add s;
 
+fun content_of body = Buffer.empty |> fold add_content body |> Buffer.content;
+
 
 
 (** string representation **)
diff -r 386576a416ea -r ccb223a4d49c src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -108,7 +108,7 @@
 
 fun pgml_terms (XML.Elem ((name, atts), body)) =
       if member (op =) token_markups name then
-        let val content = pgml_syms (Buffer.content (fold XML.add_content body Buffer.empty))
+        let val content = pgml_syms (XML.content_of body)
         in [Pgml.Atoms {kind = SOME name, content = content}] end
       else
         let val content = maps pgml_terms body in
diff -r 386576a416ea -r ccb223a4d49c src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Sep 20 12:03:11 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 20 15:08:51 2010 +0200
@@ -167,7 +167,7 @@
 fun read_token str =
   let
     val tree = YXML.parse str handle Fail msg => error msg;
-    val text = Buffer.empty |> XML.add_content tree |> Buffer.content;
+    val text = XML.content_of [tree];
     val pos =
       (case tree of
         XML.Elem ((name, props), _) =>