src/Pure/PIDE/xml.scala
changeset 49465 76ecbc7f3683
parent 49417 c5a8592fb5d3
child 49466 99ed1f422635
     1.1 --- a/src/Pure/PIDE/xml.scala	Thu Sep 20 06:48:37 2012 +0200
     1.2 +++ b/src/Pure/PIDE/xml.scala	Thu Sep 20 10:43:04 2012 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4  
     1.5    private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
     1.6    {
     1.7 -    var text = new StringBuilder
     1.8 +    val text = new StringBuilder
     1.9      var markup_tree = Markup_Tree.empty
    1.10  
    1.11      def traverse(tree: Tree): Unit =