src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Thu Sep 20 06:48:37 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Sep 20 10:43:04 2012 +0200
@@ -73,7 +73,7 @@
 
   private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
   {
-    var text = new StringBuilder
+    val text = new StringBuilder
     var markup_tree = Markup_Tree.empty
 
     def traverse(tree: Tree): Unit =