tuned;
authorwenzelm
Thu Sep 20 10:43:04 2012 +0200 (2012-09-20 ago)
changeset 4946576ecbc7f3683
parent 49464 4e4bdd12280f
child 49466 99ed1f422635
tuned;
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/xml.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 06:48:37 2012 +0200
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Sep 20 10:43:04 2012 +0200
     1.3 @@ -162,15 +162,13 @@
     1.4        List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
     1.5    }
     1.6  
     1.7 -  def swing_tree(parent: DefaultMutableTreeNode)
     1.8 -    (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
     1.9 +  def swing_tree(parent: DefaultMutableTreeNode,
    1.10 +    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
    1.11    {
    1.12      for ((_, entry) <- branches) {
    1.13 -      var current = parent
    1.14        val node = swing_node(Text.Info(entry.range, entry.markup))
    1.15 -      current.add(node)
    1.16 -      current = node
    1.17 -      entry.subtree.swing_tree(current)(swing_node)
    1.18 +      entry.subtree.swing_tree(node, swing_node)
    1.19 +      parent.add(node)
    1.20      }
    1.21    }
    1.22  }
     2.1 --- a/src/Pure/PIDE/xml.scala	Thu Sep 20 06:48:37 2012 +0200
     2.2 +++ b/src/Pure/PIDE/xml.scala	Thu Sep 20 10:43:04 2012 +0200
     2.3 @@ -73,7 +73,7 @@
     2.4  
     2.5    private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
     2.6    {
     2.7 -    var text = new StringBuilder
     2.8 +    val text = new StringBuilder
     2.9      var markup_tree = Markup_Tree.empty
    2.10  
    2.11      def traverse(tree: Tree): Unit =
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 20 06:48:37 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Sep 20 10:43:04 2012 +0200
     3.3 @@ -198,7 +198,7 @@
     3.4          val root = data.root
     3.5          for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     3.6            snapshot.state.command_state(snapshot.version, command).markup
     3.7 -            .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
     3.8 +            .swing_tree(root, (info: Text.Info[List[XML.Elem]]) =>
     3.9                {
    3.10                  val range = info.range + command_start
    3.11                  val content = command.source(info.range).replace('\n', ' ')