src/Pure/General/xml.scala

--- a/src/Pure/General/xml.scala	Thu May 06 21:02:34 2010 +0200
+++ b/src/Pure/General/xml.scala	Thu May 06 22:54:25 2010 +0200
@@ -92,6 +92,12 @@
     }
   }
 
+  def content_length(tree: XML.Tree): Int =
+    tree match {
+      case Elem(_, _, body) => (0 /: body)(_ + content_length(_))
+      case Text(s) => s.length
+    }
+
 
   /* cache for partial sharing -- NOT THREAD SAFE */