# HG changeset patch
# User wenzelm
# Date 1365092400 -7200
# Node ID a3577cd80c41402b67fc5b1f4c64448dd017d349
# Parent  4e49bba9772d055c9cddce24f422406adaa532fb
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;

diff -r 4e49bba9772d -r a3577cd80c41 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Thu Apr 04 18:06:48 2013 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Thu Apr 04 18:20:00 2013 +0200
@@ -8,8 +8,6 @@
 
 package isabelle
 
-import java.lang.System
-import javax.swing.tree.DefaultMutableTreeNode
 
 import scala.collection.immutable.SortedMap
 import scala.collection.mutable
@@ -132,7 +130,7 @@
 }
 
 
-final class Markup_Tree private(private val branches: Markup_Tree.Branches.T)
+final class Markup_Tree private(val branches: Markup_Tree.Branches.T)
 {
   import Markup_Tree._
 
@@ -280,15 +278,5 @@
     stream(root_range.start,
       List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
   }
-
-  def swing_tree(parent: DefaultMutableTreeNode,
-    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
-  {
-    for ((_, entry) <- branches) {
-      val node = swing_node(Text.Info(entry.range, entry.markup))
-      entry.subtree.swing_tree(node, swing_node)
-      parent.add(node)
-    }
-  }
 }
 
diff -r 4e49bba9772d -r a3577cd80c41 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 04 18:06:48 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 04 18:20:00 2013 +0200
@@ -44,6 +44,16 @@
     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)
+    }
+  }
 }
 
 
@@ -195,8 +205,9 @@
       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', ' ')