# HG changeset patch
# User wenzelm
# Date 1334760780 -7200
# Node ID 436ae5ea4f8049441feee21d60959a179567be3c
# Parent  1f0ec5b8135a21911a63aa8e959151234b2ff589
flat presentation of collective markup;

diff -r 1f0ec5b8135a -r 436ae5ea4f80 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)
     }
   }
diff -r 1f0ec5b8135a -r 436ae5ea4f80 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 15:09:07 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Apr 18 16:53:00 2012 +0200
@@ -155,15 +155,12 @@
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
       snapshot.state.command_state(snapshot.version, command).markup
-        .swing_tree(root)((info: Text.Markup) =>
+        .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
           {
             val range = info.range + command_start
             val content = command.source(info.range).replace('\n', ' ')
             val info_text =
-              info.info match {
-                case elem @ XML.Elem(_, _) => Pretty.formatted(List(elem), margin = 40).mkString
-                case x => x.toString
-              }
+              Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40).mkString
 
             new DefaultMutableTreeNode(
               new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {