tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
authorwenzelm
Thu Apr 04 18:20:00 2013 +0200 (2013-04-04)
changeset 51618a3577cd80c41
parent 51617 4e49bba9772d
child 51619 95b7da3430d4
tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Apr 04 18:06:48 2013 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Apr 04 18:20:00 2013 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 -import java.lang.System
     1.8 -import javax.swing.tree.DefaultMutableTreeNode
     1.9  
    1.10  import scala.collection.immutable.SortedMap
    1.11  import scala.collection.mutable
    1.12 @@ -132,7 +130,7 @@
    1.13  }
    1.14  
    1.15  
    1.16 -final class Markup_Tree private(private val branches: Markup_Tree.Branches.T)
    1.17 +final class Markup_Tree private(val branches: Markup_Tree.Branches.T)
    1.18  {
    1.19    import Markup_Tree._
    1.20  
    1.21 @@ -280,15 +278,5 @@
    1.22      stream(root_range.start,
    1.23        List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
    1.24    }
    1.25 -
    1.26 -  def swing_tree(parent: DefaultMutableTreeNode,
    1.27 -    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    1.28 -  {
    1.29 -    for ((_, entry) <- branches) {
    1.30 -      val node = swing_node(Text.Info(entry.range, entry.markup))
    1.31 -      entry.subtree.swing_tree(node, swing_node)
    1.32 -      parent.add(node)
    1.33 -    }
    1.34 -  }
    1.35  }
    1.36  
     2.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 04 18:06:48 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Apr 04 18:20:00 2013 +0200
     2.3 @@ -44,6 +44,16 @@
     2.4      override def setEnd(end: Position) = _end = end
     2.5      override def toString = _name
     2.6    }
     2.7 +
     2.8 +  def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
     2.9 +    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    2.10 +  {
    2.11 +    for ((_, entry) <- tree.branches) {
    2.12 +      val node = swing_node(Text.Info(entry.range, entry.markup))
    2.13 +      swing_markup_tree(entry.subtree, node, swing_node)
    2.14 +      parent.add(node)
    2.15 +    }
    2.16 +  }
    2.17  }
    2.18  
    2.19  
    2.20 @@ -195,8 +205,9 @@
    2.21        case Some(snapshot) =>
    2.22          val root = data.root
    2.23          for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
    2.24 -          snapshot.state.command_state(snapshot.version, command).markup
    2.25 -            .swing_tree(root, (info: Text.Info[List[XML.Elem]]) =>
    2.26 +          Isabelle_Sidekick.swing_markup_tree(
    2.27 +            snapshot.state.command_state(snapshot.version, command).markup, root,
    2.28 +              (info: Text.Info[List[XML.Elem]]) =>
    2.29                {
    2.30                  val range = info.range + command_start
    2.31                  val content = command.source(info.range).replace('\n', ' ')