# HG changeset patch
# User wenzelm
# Date 1348130584 -7200
# Node ID 76ecbc7f36832be6a7ec0e0b32107579208a1dbc
# Parent  4e4bdd12280f76b524ed61da0181c9e05a626ed8
tuned;

diff -r 4e4bdd12280f -r 76ecbc7f3683 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 06:48:37 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 10:43:04 2012 +0200
@@ -162,15 +162,13 @@
       List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   }
 
-  def swing_tree(parent: DefaultMutableTreeNode)
-    (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
+  def swing_tree(parent: DefaultMutableTreeNode,
+    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
   {
     for ((_, entry) <- branches) {
-      var current = parent
       val node = swing_node(Text.Info(entry.range, entry.markup))
-      current.add(node)
-      current = node
-      entry.subtree.swing_tree(current)(swing_node)
+      entry.subtree.swing_tree(node, swing_node)
+      parent.add(node)
     }
   }
 }
diff -r 4e4bdd12280f -r 76ecbc7f3683 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 =
diff -r 4e4bdd12280f -r 76ecbc7f3683 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 20 06:48:37 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 20 10:43:04 2012 +0200
@@ -198,7 +198,7 @@
         val root = data.root
         for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
           snapshot.state.command_state(snapshot.version, command).markup
-            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
+            .swing_tree(root, (info: Text.Info[List[XML.Elem]]) =>
               {
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')