# HG changeset patch
# User wenzelm
# Date 1273160997 -7200
# Node ID 943f1ca7b375762665d6e9b75a1e15fe8d1dab6c
# Parent  41a1210519fdc5c8e5a66a3a1c15c2423968c3e2
misc tuning -- accumulate body via ListBuffer;

diff -r 41a1210519fd -r 943f1ca7b375 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu May 06 16:27:47 2010 +0200
+++ b/src/Pure/General/yxml.scala	Thu May 06 17:49:57 2010 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import scala.collection.mutable.ListBuffer
+
+
 object YXML
 {
   /* chunk markers */
@@ -83,26 +86,32 @@
   {
     /* stack operations */
 
-    var stack: List[((String, XML.Attributes), List[XML.Tree])] = null
+    def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
+    var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
 
-    def add(x: XML.Tree) = (stack: @unchecked) match {
-      case ((elem, body) :: pending) => stack = (elem, x :: body) :: pending
+    def add(x: XML.Tree)
+    {
+      (stack: @unchecked) match { case ((_, body) :: _) => body += x }
     }
 
-    def push(name: String, atts: XML.Attributes) =
+    def push(name: String, atts: XML.Attributes)
+    {
       if (name == "") err_element()
-      else stack = ((name, atts), Nil) :: stack
+      else stack = ((name, atts), buffer()) :: stack
+    }
 
-    def pop() = (stack: @unchecked) match {
-      case ((("", _), _) :: _) => err_unbalanced("")
-      case (((name, atts), body) :: pending) =>
-        stack = pending; add(XML.Elem(name, atts, body.reverse))
+    def pop()
+    {
+      (stack: @unchecked) match {
+        case ((("", _), _) :: _) => err_unbalanced("")
+        case (((name, atts), body) :: pending) =>
+          stack = pending; add(XML.Elem(name, atts, body.toList))
+      }
     }
 
 
     /* parse chunks */
 
-    stack = List((("", Nil), Nil))
     for (chunk <- chunks(X, source) if chunk.length != 0) {
       if (chunk.length == 1 && chunk.charAt(0) == Y) pop()
       else {
@@ -114,7 +123,7 @@
       }
     }
     stack match {
-      case List((("", _), result)) => result.reverse
+      case List((("", _), body)) => body.toList
       case ((name, _), _) :: _ => err_unbalanced(name)
     }
   }