# HG changeset patch
# User wenzelm
# Date 1273179265 -7200
# Node ID b1956bc8f5857b9be5b319904eb5a177f9fc4cdb
# Parent  2b3076cfd6ddb580112b346690bf8998b194f646
added content_length;

diff -r 2b3076cfd6dd -r b1956bc8f585 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 */