src/Pure/PIDE/markup_tree.scala
author wenzelm
Thu, 26 Aug 2010 11:31:21 +0200
changeset 38726 6d5f9af42eca
parent 38661 f1ba2ae8e58a
child 38845 a9e37daf5bd0
permissions -rw-r--r--
Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
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
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     2
    Author:     Fabian Immler, TU Munich
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     3
    Author:     Makarius
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     4
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
     5
Markup trees over nested / non-overlapping text ranges.
36676
ac7961d42ac3 some rearrangement of Scala sources;
wenzelm
parents: 36012
diff changeset
     6
*/
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     7
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
     8
package isabelle
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
     9
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    10
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    11
import javax.swing.tree.DefaultMutableTreeNode
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    12
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    13
import scala.collection.immutable.SortedMap
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    14
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
object Markup_Tree
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    17
{
38566
8176107637ce Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents: 38564
diff changeset
    18
  /* branches sorted by quasi-order -- overlapping ranges appear as equivalent */
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    19
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    20
  object Branches
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    21
  {
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    22
    type Entry = (Text.Info[Any], Markup_Tree)
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    23
    type T = SortedMap[Text.Range, Entry]
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    24
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    25
    val empty = SortedMap.empty[Text.Range, Entry](new scala.math.Ordering[Text.Range]
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    26
      {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    27
        def compare(r1: Text.Range, r2: Text.Range): Int = r1 compare r2
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    28
      })
38562
3de5f0424caa misc tuning and simplification;
wenzelm
parents: 38486
diff changeset
    29
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    30
    def update(branches: T, entry: Entry): T = branches + (entry._1.range -> entry)
38657
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    31
    def single(entry: Entry): T = update(empty, entry)
38562
3de5f0424caa misc tuning and simplification;
wenzelm
parents: 38486
diff changeset
    32
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    33
    def overlapping(range: Text.Range, branches: T): T =  // FIXME special cases!?
38566
8176107637ce Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents: 38564
diff changeset
    34
    {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    35
      val start = Text.Range(range.start)
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    36
      val stop = Text.Range(range.stop)
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    37
      val bs = branches.range(start, stop)
38566
8176107637ce Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents: 38564
diff changeset
    38
      branches.get(stop) match {
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    39
        case Some(end) if range overlaps end._1.range => update(bs, end)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    40
        case _ => bs
38566
8176107637ce Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents: 38564
diff changeset
    41
      }
8176107637ce Branches.overlapping: proper treatment of stop_range that overlaps with end;
wenzelm
parents: 38564
diff changeset
    42
    }
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    43
  }
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
  val empty = new Markup_Tree(Branches.empty)
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    46
}
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
    47
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
    48
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    49
case class Markup_Tree(val 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
    50
{
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    51
  import Markup_Tree._
34557
647a2430d1cd immutable markup-nodes;
immler@in.tum.de
parents: 34555
diff changeset
    52
38563
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    53
  override def toString =
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    54
    branches.toList.map(_._2) match {
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    55
      case Nil => "Empty"
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    56
      case list => list.mkString("Tree(", ",", ")")
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    57
    }
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
    58
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    59
  def + (new_info: Text.Info[Any]): Markup_Tree =
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    60
  {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    61
    val new_range = new_info.range
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    62
    branches.get(new_range) match {
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    63
      case None =>
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    64
        new Markup_Tree(Branches.update(branches, new_info -> empty))
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    65
      case Some((info, subtree)) =>
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    66
        val range = info.range
38661
f1ba2ae8e58a Markup_Tree.+: new info tends to sink to bottom, where it is prefered by select;
wenzelm
parents: 38659
diff changeset
    67
        if (range.contains(new_range))
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    68
          new Markup_Tree(Branches.update(branches, info -> (subtree + new_info)))
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    69
        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
38657
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    70
          new Markup_Tree(Branches.single(new_info -> this))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    71
        else {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    72
          val body = Branches.overlapping(new_range, branches)
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    73
          if (body.forall(e => new_range.contains(e._1))) {
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    74
            val rest = // branches -- body, modulo workarounds for Redblack in Scala 2.8.0
38657
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    75
              if (body.size > 1)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    76
                (Branches.empty /: branches)((rest, entry) =>
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    77
                  if (body.isDefinedAt(entry._1)) rest else rest + entry)
2e0ebdaac59b misc tuning of important special cases;
wenzelm
parents: 38584
diff changeset
    78
              else branches
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    79
            new Markup_Tree(Branches.update(rest, new_info -> new Markup_Tree(body)))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    80
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    81
          else { // FIXME split markup!?
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
    82
            System.err.println("Ignored overlapping markup information: " + new_info)
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    83
            this
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    84
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
    85
        }
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    86
    }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    87
  }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
    88
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    89
  private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    90
    Branches.overlapping(range, branches).toStream
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    91
38582
3a6ce43d99b1 tuned signature;
wenzelm
parents: 38578
diff changeset
    92
  def select[A](root_range: Text.Range)
3a6ce43d99b1 tuned signature;
wenzelm
parents: 38578
diff changeset
    93
    (result: PartialFunction[Text.Info[Any], A])(default: A): Stream[Text.Info[A]] =
38486
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
    94
  {
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    95
    def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    96
      : Stream[Text.Info[A]] =
38486
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
    97
    {
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    98
      stack match {
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
    99
        case (parent, (range, (info, tree)) #:: more) :: rest =>
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   100
          val subrange = range.restrict(root_range)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   101
          val subtree = tree.overlapping(subrange)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   102
          val start = subrange.start
38486
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
   103
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   104
          if (result.isDefinedAt(info)) {
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   105
            val next = Text.Info(subrange, result(info))
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   106
            val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   107
            if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   108
            else nexts
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   109
          }
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   110
          else stream(last, (parent, subtree #::: more) :: rest)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   111
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   112
        case (parent, Stream.Empty) :: rest =>
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   113
          val stop = parent.range.stop
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   114
          val nexts = stream(stop, rest)
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   115
          if (last < stop) parent.restrict(Text.Range(last, stop)) #:: nexts
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   116
          else nexts
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   117
38726
6d5f9af42eca Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents: 38661
diff changeset
   118
        case Nil =>
6d5f9af42eca Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents: 38661
diff changeset
   119
          val stop = root_range.stop
6d5f9af42eca Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents: 38661
diff changeset
   120
          if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
6d5f9af42eca Markup_Tree.select: uniform treatment of root_range wrt. singularities, yielding empty result stream;
wenzelm
parents: 38661
diff changeset
   121
          else Stream.empty
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   122
      }
38486
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
   123
    }
38659
afac51977705 Markup_Tree.select: more straight-forward recursion producing one main stream, avoid fragmentation of parent info due to ignored subtree;
wenzelm
parents: 38657
diff changeset
   124
    stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
38486
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
   125
  }
f5bbfc019937 Markup_Tree.select: crude version of stream-based filtering;
wenzelm
parents: 38482
diff changeset
   126
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
   127
  def swing_tree(parent: DefaultMutableTreeNode)
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
   128
    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   129
  {
38577
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
   130
    for ((_, (info, subtree)) <- branches) {
4e4d3ea3725a renamed Markup_Tree.Node to Text.Info;
wenzelm
parents: 38576
diff changeset
   131
      val current = swing_node(info)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   132
      subtree.swing_tree(current)(swing_node)
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   133
      parent.add(current)
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   134
    }
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   135
  }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   136
}
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   137