src/Pure/PIDE/markup_tree.scala
author wenzelm
Tue, 29 Nov 2011 21:50:00 +0100
changeset 45674 eb65c9d17e2f
parent 45673 cd41e3903fbf
child 46165 0e131ca93a49
permissions -rw-r--r--
clarified Time vs. Timing;
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
{
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    19
  sealed case class Cumulate[A](
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    20
    info: A, result: PartialFunction[(A, Text.Markup), A], elements: Option[Set[String]])
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    21
  sealed case class Select[A](
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    22
    result: PartialFunction[Text.Markup, A], elements: Option[Set[String]])
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    23
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    24
  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
    25
45473
wenzelm
parents: 45470
diff changeset
    26
  object Entry
wenzelm
parents: 45470
diff changeset
    27
  {
wenzelm
parents: 45470
diff changeset
    28
    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
    29
      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
45473
wenzelm
parents: 45470
diff changeset
    30
  }
wenzelm
parents: 45470
diff changeset
    31
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    32
  sealed case class Entry(
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    33
    range: Text.Range,
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    34
    rev_markup: List[XML.Elem],
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    35
    elements: Set[String],
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    36
    subtree: Markup_Tree)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    37
  {
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    38
    def + (info: XML.Elem): Entry =
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    39
      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
    40
      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
    41
45470
81b85d4ed269 more precise type;
wenzelm
parents: 45469
diff changeset
    42
    def markup: List[XML.Elem] = rev_markup.reverse
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    43
  }
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    44
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    45
  object Branches
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    46
  {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    47
    type T = SortedMap[Text.Range, Entry]
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    48
    val empty: T = SortedMap.empty(Text.Range.Ordering)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    49
  }
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    50
}
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    51
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    52
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    53
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
    54
{
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    55
  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
    56
    this(branches + (entry.range -> entry))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    57
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    58
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    59
  import Markup_Tree._
34557
647a2430d1cd immutable markup-nodes;
immler@in.tum.de
parents: 34555
diff changeset
    60
38563
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    61
  override def toString =
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    62
    branches.toList.map(_._2) match {
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    63
      case Nil => "Empty"
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    64
      case list => list.mkString("Tree(", ",", ")")
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    65
    }
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    66
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    67
  private def overlapping(range: Text.Range): Branches.T =
45457
wenzelm
parents: 45456
diff changeset
    68
  {
wenzelm
parents: 45456
diff changeset
    69
    val start = Text.Range(range.start)
wenzelm
parents: 45456
diff changeset
    70
    val stop = Text.Range(range.stop)
wenzelm
parents: 45456
diff changeset
    71
    val bs = branches.range(start, stop)
wenzelm
parents: 45456
diff changeset
    72
    // FIXME check after Scala 2.8.x
wenzelm
parents: 45456
diff changeset
    73
    branches.get(stop) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    74
      case Some(end) if range overlaps end.range => bs + (end.range -> end)
45457
wenzelm
parents: 45456
diff changeset
    75
      case _ => bs
wenzelm
parents: 45456
diff changeset
    76
    }
wenzelm
parents: 45456
diff changeset
    77
  }
wenzelm
parents: 45456
diff changeset
    78
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    79
  def + (new_markup: Text.Markup): Markup_Tree =
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    80
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    81
    val new_range = new_markup.range
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    82
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    83
    branches.get(new_range) match {
45473
wenzelm
parents: 45470
diff changeset
    84
      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
    85
      case Some(entry) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    86
        if (entry.range == new_range)
45473
wenzelm
parents: 45470
diff changeset
    87
          new Markup_Tree(branches, entry + new_markup.info)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    88
        else if (entry.range.contains(new_range))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    89
          new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    90
        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
45473
wenzelm
parents: 45470
diff changeset
    91
          new Markup_Tree(Branches.empty, Entry(new_markup, this))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    92
        else {
45457
wenzelm
parents: 45456
diff changeset
    93
          val body = overlapping(new_range)
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    94
          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
    95
            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
    96
              if (body.size > 1)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    97
                (Branches.empty /: branches)((rest, entry) =>
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    98
                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    99
              else branches
45473
wenzelm
parents: 45470
diff changeset
   100
            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
   101
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   102
          else { // FIXME split markup!?
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   103
            System.err.println("Ignored overlapping markup information: " + new_markup)
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   104
            this
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   105
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   106
        }
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   107
    }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   108
  }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   109
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   110
  def cumulate[A](root_range: Text.Range)(body: Cumulate[A]): Stream[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   111
  {
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   112
    val root_info = body.info
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   113
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   114
    def result(x: A, entry: Entry): Option[A] =
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   115
      if (body.elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   116
        val (y, changed) =
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   117
          (entry.markup :\ (x, false))((info, res) =>
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   118
            {
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   119
              val (y, changed) = res
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   120
              val arg = (x, Text.Info(entry.range, info))
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   121
              if (body.result.isDefinedAt(arg)) (body.result(arg), true)
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   122
              else res
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   123
            })
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
   124
        if (changed) Some(y) else None
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
      else None
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   127
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   128
    def stream(
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   129
      last: Text.Offset,
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   130
      stack: List[(Text.Info[A], Stream[(Text.Range, Entry)])]): Stream[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   131
    {
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   132
      stack match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   133
        case (parent, (range, entry) #:: more) :: rest =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   134
          val subrange = range.restrict(root_range)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   135
          val subtree = entry.subtree.overlapping(subrange).toStream
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   136
          val start = subrange.start
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   137
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   138
          result(parent.info, entry) match {
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   139
            case Some(res) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   140
              val next = Text.Info(subrange, res)
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   141
              val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   142
              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
   143
              else nexts
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   144
            case None => stream(last, (parent, subtree #::: more) :: rest)
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   145
          }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   146
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   147
        case (parent, Stream.Empty) :: rest =>
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   148
          val stop = parent.range.stop
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   149
          val nexts = stream(stop, rest)
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   150
          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   151
          else nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   152
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   153
        case Nil =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   154
          val stop = root_range.stop
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   155
          if (last < stop) Stream(Text.Info(Text.Range(last, stop), root_info))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   156
          else Stream.empty
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   157
      }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   158
    }
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   159
    stream(root_range.start,
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   160
      List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   161
  }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   162
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
   163
  def swing_tree(parent: DefaultMutableTreeNode)
45455
4f974c0c5c2f prefer statically typed Text.Markup;
wenzelm
parents: 44379
diff changeset
   164
    (swing_node: Text.Markup => DefaultMutableTreeNode)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   165
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   166
    for ((_, entry) <- branches) {
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   167
      var current = parent
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   168
      for (info <- entry.markup) {
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   169
        val node = swing_node(Text.Info(entry.range, info))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   170
        current.add(node)
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   171
        current = node
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   172
      }
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   173
      entry.subtree.swing_tree(current)(swing_node)
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   174
    }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   175
  }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   176
}
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   177