src/Pure/PIDE/markup_tree.scala
changeset 47539 436ae5ea4f80
parent 46712 8650d9a95736
child 48762 9ff86bf6ad19
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 15:09:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Apr 18 16:53:00 2012 +0200
     1.3 @@ -155,15 +155,13 @@
     1.4    }
     1.5  
     1.6    def swing_tree(parent: DefaultMutableTreeNode)
     1.7 -    (swing_node: Text.Markup => DefaultMutableTreeNode)
     1.8 +    (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
     1.9    {
    1.10      for ((_, entry) <- branches) {
    1.11        var current = parent
    1.12 -      for (info <- entry.markup) {
    1.13 -        val node = swing_node(Text.Info(entry.range, info))
    1.14 -        current.add(node)
    1.15 -        current = node
    1.16 -      }
    1.17 +      val node = swing_node(Text.Info(entry.range, entry.markup))
    1.18 +      current.add(node)
    1.19 +      current = node
    1.20        entry.subtree.swing_tree(current)(swing_node)
    1.21      }
    1.22    }