src/Pure/PIDE/markup_tree.scala

--- a/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 15:09:07 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 16:53:00 2012 +0200
@@ -155,15 +155,13 @@
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
-    (swing_node: Text.Markup => DefaultMutableTreeNode)
+    (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
   {
     for ((_, entry) <- branches) {
       var current = parent
-      for (info <- entry.markup) {
-        val node = swing_node(Text.Info(entry.range, info))
-        current.add(node)
-        current = node
-      }
+      val node = swing_node(Text.Info(entry.range, entry.markup))
+      current.add(node)
+      current = node
       entry.subtree.swing_tree(current)(swing_node)
     }
   }