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