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    }

     2.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 15:09:07 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 16:53:00 2012 +0200
     2.3 @@ -155,15 +155,12 @@
     2.4      val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     2.5      for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     2.6        snapshot.state.command_state(snapshot.version, command).markup
     2.7 -        .swing_tree(root)((info: Text.Markup) =>
     2.8 +        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
     2.9            {
    2.10              val range = info.range + command_start
    2.11              val content = command.source(info.range).replace('\n', ' ')
    2.12              val info_text =
    2.13 -              info.info match {
    2.14 -                case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString
    2.15 -                case x => x.toString
    2.16 -              }
    2.17 +              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
    2.18  
    2.19              new DefaultMutableTreeNode(
    2.20                new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {