src/Tools/jEdit/src/isabelle_sidekick.scala

     override def getStart: Position = _start
     override def setStart(start: Position) = _start = start
     override def getEnd: Position = _end
     override def setEnd(end: Position) = _end = end
     override def toString = _name
+  }
+
+  def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
+    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
+  {
+    for ((_, entry) <- tree.branches) {
+      val node = swing_node(Text.Info(entry.range, entry.markup))
+      swing_markup_tree(entry.subtree, node, swing_node)
+      parent.add(node)
+    }
   }
 }
 
 
 class Isabelle_Sidekick(name: String, get_syntax: => Option[Outer_Syntax])

   {
     Swing_Thread.now { Document_Model(buffer).map(_.snapshot) } match {
       case Some(snapshot) =>
         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]]) =>
+          Isabelle_Sidekick.swing_markup_tree(
+            snapshot.state.command_state(snapshot.version, command).markup, root,
+              (info: Text.Info[List[XML.Elem]]) =>
               {
                 val range = info.range + command_start
                 val content = command.source(info.range).replace('\n', ' ')
                 val info_text =
                   Pretty.formatted(Library.separate(Pretty.FBreak, info.info), margin = 40.0)