src/Pure/PIDE/markup_tree.scala
author wenzelm
Thu, 20 Sep 2012 10:43:04 +0200
changeset 49465 76ecbc7f3683
parent 49417 c5a8592fb5d3
child 49466 99ed1f422635
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
     1
/*  Title:      Pure/PIDE/markup_tree.scala
45673
cd41e3903fbf separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
wenzelm
parents: 45667
diff changeset
     2
    Module:     PIDE
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     5
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
     6
Markup trees over nested / non-overlapping text ranges.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     7
*/
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     8
34871
e596a0b71f3c incorporate "proofdocument" part into main Isabelle/Pure.jar -- except for html_panel.scala, which depends on external library (Lobo/Cobra browser);
wenzelm
parents: 34760
diff changeset
     9
package isabelle
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    10
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 39178
diff changeset
    11
import java.lang.System
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    12
import javax.swing.tree.DefaultMutableTreeNode
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    13
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    14
import scala.collection.immutable.SortedMap
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    15
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    16
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    17
object Markup_Tree
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    18
{
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    19
  val empty: Markup_Tree = new Markup_Tree(Branches.empty)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    20
45473
wenzelm
parents: 45470
diff changeset
    21
  object Entry
wenzelm
parents: 45470
diff changeset
    22
  {
wenzelm
parents: 45470
diff changeset
    23
    def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    24
      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
45473
wenzelm
parents: 45470
diff changeset
    25
  }
wenzelm
parents: 45470
diff changeset
    26
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    27
  sealed case class Entry(
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    28
    range: Text.Range,
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    29
    rev_markup: List[XML.Elem],
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    30
    elements: Set[String],
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    31
    subtree: Markup_Tree)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    32
  {
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    33
    def + (info: XML.Elem): Entry =
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    34
      if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    35
      else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    36
45470
81b85d4ed269 more precise type;
wenzelm
parents: 45469
diff changeset
    37
    def markup: List[XML.Elem] = rev_markup.reverse
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    38
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    39
    def reverse_markup: Entry =
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    40
      copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    41
  }
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    42
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    43
  object Branches
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    44
  {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    45
    type T = SortedMap[Text.Range, Entry]
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    46
    val empty: T = SortedMap.empty(Text.Range.Ordering)
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    47
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    48
    def reverse_markup(branches: T): T =
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    49
      (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    50
  }
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    51
}
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    52
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    53
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46178
diff changeset
    54
final class Markup_Tree private(branches: Markup_Tree.Branches.T)
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
    55
{
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    56
  import Markup_Tree._
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    57
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    58
  private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    59
    this(branches + (entry.range -> entry))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    60
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
    61
  def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
34557
647a2430d1cd immutable markup-nodes;
immler@in.tum.de
parents: 34555
diff changeset
    62
38563
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    63
  override def toString =
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    64
    branches.toList.map(_._2) match {
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    65
      case Nil => "Empty"
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    66
      case list => list.mkString("Tree(", ",", ")")
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    67
    }
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    68
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    69
  private def overlapping(range: Text.Range): Branches.T =
45457
wenzelm
parents: 45456
diff changeset
    70
  {
wenzelm
parents: 45456
diff changeset
    71
    val start = Text.Range(range.start)
wenzelm
parents: 45456
diff changeset
    72
    val stop = Text.Range(range.stop)
wenzelm
parents: 45456
diff changeset
    73
    val bs = branches.range(start, stop)
wenzelm
parents: 45456
diff changeset
    74
    // FIXME check after Scala 2.8.x
wenzelm
parents: 45456
diff changeset
    75
    branches.get(stop) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    76
      case Some(end) if range overlaps end.range => bs + (end.range -> end)
45457
wenzelm
parents: 45456
diff changeset
    77
      case _ => bs
wenzelm
parents: 45456
diff changeset
    78
    }
wenzelm
parents: 45456
diff changeset
    79
  }
wenzelm
parents: 45456
diff changeset
    80
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    81
  def + (new_markup: Text.Markup): Markup_Tree =
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    82
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    83
    val new_range = new_markup.range
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    84
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    85
    branches.get(new_range) match {
45473
wenzelm
parents: 45470
diff changeset
    86
      case None => new Markup_Tree(branches, Entry(new_markup, empty))
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    87
      case Some(entry) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    88
        if (entry.range == new_range)
45473
wenzelm
parents: 45470
diff changeset
    89
          new Markup_Tree(branches, entry + new_markup.info)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    90
        else if (entry.range.contains(new_range))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    91
          new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    92
        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
45473
wenzelm
parents: 45470
diff changeset
    93
          new Markup_Tree(Branches.empty, Entry(new_markup, this))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    94
        else {
45457
wenzelm
parents: 45456
diff changeset
    95
          val body = overlapping(new_range)
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    96
          if (body.forall(e => new_range.contains(e._1))) {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    97
            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0 FIXME
38657
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    98
              if (body.size > 1)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    99
                (Branches.empty /: branches)((rest, entry) =>
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
   100
                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
   101
              else branches
45473
wenzelm
parents: 45470
diff changeset
   102
            new Markup_Tree(rest, Entry(new_markup, new Markup_Tree(body)))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   103
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   104
          else { // FIXME split markup!?
48762
9ff86bf6ad19 tuned message;
wenzelm
parents: 47539
diff changeset
   105
            System.err.println("Ignored overlapping markup information: " + new_markup +
9ff86bf6ad19 tuned message;
wenzelm
parents: 47539
diff changeset
   106
              body.filter(e => !new_range.contains(e._1)).mkString("\n"))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   107
            this
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   108
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   109
        }
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   110
    }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   111
  }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   112
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   113
  def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   114
    result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   115
  {
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   116
    def results(x: A, entry: Entry): Option[A] =
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   117
      if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   118
        val (y, changed) =
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   119
          (entry.markup :\ (x, false))((info, res) =>
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   120
            {
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   121
              val (y, changed) = res
46165
0e131ca93a49 proper cumulation of bulk arguments;
wenzelm
parents: 45673
diff changeset
   122
              val arg = (y, Text.Info(entry.range, info))
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   123
              if (result.isDefinedAt(arg)) (result(arg), true)
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   124
              else res
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   125
            })
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   126
        if (changed) Some(y) else None
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   127
      }
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   128
      else None
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   129
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   130
    def stream(
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   131
      last: Text.Offset,
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   132
      stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   133
    {
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   134
      stack match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   135
        case (parent, (range, entry) #:: more) :: rest =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   136
          val subrange = range.restrict(root_range)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   137
          val subtree = entry.subtree.overlapping(subrange).toStream
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   138
          val start = subrange.start
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   139
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   140
          results(parent.info, entry) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   141
            case Some(res) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   142
              val next = Text.Info(subrange, res)
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   143
              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   144
              if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   145
              else nexts
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   146
            case None => stream(last, (parent, subtree #::: more) :: rest)
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   147
          }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   148
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   149
        case (parent, Stream.Empty) :: rest =>
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   150
          val stop = parent.range.stop
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   151
          val nexts = stream(stop, rest)
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   152
          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   153
          else nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   154
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   155
        case Nil =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   156
          val stop = root_range.stop
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   157
          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   158
          else Stream.empty
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   159
      }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   160
    }
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   161
    stream(root_range.start,
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   162
      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   163
  }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   164
49465
wenzelm
parents: 49417
diff changeset
   165
  def swing_tree(parent: DefaultMutableTreeNode,
wenzelm
parents: 49417
diff changeset
   166
    swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   167
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   168
    for ((_, entry) <- branches) {
47539
436ae5ea4f80 flat presentation of collective markup;
wenzelm
parents: 46712
diff changeset
   169
      val node = swing_node(Text.Info(entry.range, entry.markup))
49465
wenzelm
parents: 49417
diff changeset
   170
      entry.subtree.swing_tree(node, swing_node)
wenzelm
parents: 49417
diff changeset
   171
      parent.add(node)
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   172
    }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   173
  }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   174
}
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   175