src/Pure/PIDE/markup_tree.scala
author wenzelm
Wed, 07 Aug 2013 19:59:58 +0200
changeset 52900 d29bf6db8a2d
parent 52889 ea3338812e67
child 55618 995162143ef4
permissions -rw-r--r--
more elementary list structures for markup tree traversal;
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
34701
80b0add08eef IsabelleSideKickParser: incorporate former MarkupNode.markup2default_node, observe stopped flag;
wenzelm
parents: 34676
diff changeset
    11
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    12
import scala.collection.immutable.SortedMap
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
    13
import scala.collection.mutable
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    14
import scala.annotation.tailrec
38479
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
{
50551
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    19
  /* construct trees */
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    20
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    21
  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
    22
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    23
  def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    24
    trees match {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    25
      case Nil => empty
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    26
      case head :: tail =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    27
        new Markup_Tree(
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    28
          (head.branches /: tail) {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    29
            case (branches, tree) =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    30
              (branches /: tree.branches) {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    31
                case (bs, (r, entry)) =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    32
                  require(!bs.isDefinedAt(r))
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    33
                  bs + (r -> entry)
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    34
              }
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    35
          })
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    36
    }
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    37
50551
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    38
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    39
  /* tree building blocks */
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    40
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    41
  object Elements
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    42
  {
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    43
    val empty = new Elements(Set.empty)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    44
  }
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    45
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    46
  final class Elements private(private val rep: Set[String])
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    47
  {
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    48
    def contains(name: String): Boolean = rep.contains(name)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    49
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    50
    def + (name: String): Elements =
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    51
      if (contains(name)) this
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    52
      else new Elements(rep + name)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    53
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    54
    def + (elem: XML.Elem): Elements = this + elem.markup.name
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    55
    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    56
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    57
    def ++ (other: Elements): Elements =
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    58
      if (this eq other) this
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    59
      else if (rep.isEmpty) other
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    60
      else (this /: other.rep)(_ + _)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    61
  }
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    62
45473
wenzelm
parents: 45470
diff changeset
    63
  object Entry
wenzelm
parents: 45470
diff changeset
    64
  {
wenzelm
parents: 45470
diff changeset
    65
    def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    66
      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    67
        subtree, subtree.make_elements)
49469
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
    68
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
    69
    def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    70
      Entry(range, rev_markups, Elements.empty ++ rev_markups,
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    71
        subtree, subtree.make_elements)
45473
wenzelm
parents: 45470
diff changeset
    72
  }
wenzelm
parents: 45470
diff changeset
    73
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    74
  sealed case class Entry(
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    75
    range: Text.Range,
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    76
    rev_markup: List[XML.Elem],
50551
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    77
    elements: Elements,
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    78
    subtree: Markup_Tree,
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    79
    subtree_elements: Elements)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    80
  {
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    81
    def markup: List[XML.Elem] = rev_markup.reverse
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    82
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    83
    def + (markup: Text.Markup): Entry =
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    84
      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    85
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    86
    def \ (markup: Text.Markup): Entry =
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    87
      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    88
  }
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    89
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    90
  object Branches
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    91
  {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    92
    type T = SortedMap[Text.Range, Entry]
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    93
    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
    94
  }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    95
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    96
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    97
  /* XML representation */
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    98
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
    99
  @tailrec private def strip_elems(
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   100
      elems: List[XML.Elem], body: XML.Body): (List[XML.Elem], XML.Body) =
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   101
    body match {
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   102
      case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   103
        strip_elems(XML.Elem(markup1, body1) :: elems, body2)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   104
      case List(XML.Elem(markup1, body1)) =>
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   105
        strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   106
      case _ => (elems, body)
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   107
    }
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   108
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   109
  private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   110
    {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   111
      val (offset, markup_trees) = acc
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   112
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   113
      strip_elems(Nil, List(tree)) match {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   114
        case (Nil, body) =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   115
          (offset + XML.text_length(body), markup_trees)
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
   116
49469
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
   117
        case (elems, body) =>
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
   118
          val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
50642
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   119
          if (offset == end_offset) acc
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   120
          else {
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   121
            val range = Text.Range(offset, end_offset)
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   122
            val entry = Entry(range, elems, merge_disjoint(subtrees))
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   123
            (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
aca12f646772 ignore markup elements over empty body, which are not well-defined within markup tree and fail to work with merge_disjoint (e.g. multiple inlined positions);
wenzelm
parents: 50552
diff changeset
   124
          }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
   125
      }
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   126
    }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
   127
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   128
  def from_XML(body: XML.Body): Markup_Tree =
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   129
    merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
   130
}
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
   131
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   132
51618
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 50642
diff changeset
   133
final class Markup_Tree private(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
   134
{
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
   135
  import Markup_Tree._
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
   136
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   137
  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
   138
    this(branches + (entry.range -> entry))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   139
38563
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   140
  override def toString =
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   141
    branches.toList.map(_._2) match {
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   142
      case Nil => "Empty"
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   143
      case list => list.mkString("Tree(", ",", ")")
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   144
    }
f6c9a4f9f66f added toString methods;
wenzelm
parents: 38562
diff changeset
   145
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   146
  private def overlapping(range: Text.Range): Branches.T =
45457
wenzelm
parents: 45456
diff changeset
   147
  {
wenzelm
parents: 45456
diff changeset
   148
    val start = Text.Range(range.start)
wenzelm
parents: 45456
diff changeset
   149
    val stop = Text.Range(range.stop)
wenzelm
parents: 45456
diff changeset
   150
    val bs = branches.range(start, stop)
wenzelm
parents: 45456
diff changeset
   151
    branches.get(stop) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   152
      case Some(end) if range overlaps end.range => bs + (end.range -> end)
45457
wenzelm
parents: 45456
diff changeset
   153
      case _ => bs
wenzelm
parents: 45456
diff changeset
   154
    }
wenzelm
parents: 45456
diff changeset
   155
  }
wenzelm
parents: 45456
diff changeset
   156
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   157
  def make_elements: Elements =
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   158
    (Elements.empty /: branches)(
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   159
      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   160
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   161
  def + (new_markup: Text.Markup): Markup_Tree =
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   162
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   163
    val new_range = new_markup.range
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   164
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
   165
    branches.get(new_range) match {
45473
wenzelm
parents: 45470
diff changeset
   166
      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
   167
      case Some(entry) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   168
        if (entry.range == new_range)
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   169
          new Markup_Tree(branches, entry + new_markup)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   170
        else if (entry.range.contains(new_range))
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   171
          new Markup_Tree(branches, entry \ new_markup)
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
   172
        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
45473
wenzelm
parents: 45470
diff changeset
   173
          new Markup_Tree(Branches.empty, Entry(new_markup, this))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   174
        else {
45457
wenzelm
parents: 45456
diff changeset
   175
          val body = overlapping(new_range)
49607
b610c0d52bfa updated to consolidated SortedMap in scala-2.9.x;
wenzelm
parents: 49469
diff changeset
   176
          if (body.forall(e => new_range.contains(e._1)))
b610c0d52bfa updated to consolidated SortedMap in scala-2.9.x;
wenzelm
parents: 49469
diff changeset
   177
            new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
49608
wenzelm
parents: 49607
diff changeset
   178
          else {
wenzelm
parents: 49607
diff changeset
   179
            java.lang.System.err.println("Ignored overlapping markup information: " + new_markup +
48762
9ff86bf6ad19 tuned message;
wenzelm
parents: 47539
diff changeset
   180
              body.filter(e => !new_range.contains(e._1)).mkString("\n"))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   181
            this
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   182
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   183
        }
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   184
    }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   185
  }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   186
52642
84eb792224a8 full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
wenzelm
parents: 51618
diff changeset
   187
  def ++ (other: Markup_Tree): Markup_Tree =
84eb792224a8 full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
wenzelm
parents: 51618
diff changeset
   188
    (this /: other.branches)({ case (tree, (range, entry)) =>
84eb792224a8 full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
wenzelm
parents: 51618
diff changeset
   189
      ((tree ++ entry.subtree) /: entry.markup)({ case (t, elem) => t + Text.Info(range, elem) }) })
84eb792224a8 full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);
wenzelm
parents: 51618
diff changeset
   190
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   191
  def to_XML(root_range: Text.Range, text: CharSequence, filter: XML.Elem => Boolean): XML.Body =
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   192
  {
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   193
    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   194
      if (start == stop) Nil
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   195
      else List(XML.Text(text.subSequence(start, stop).toString))
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   196
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   197
    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   198
      (body /: rev_markups) {
49650
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   199
        case (b, elem) =>
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   200
          if (!filter(elem)) b
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   201
          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
9fad6480300d support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;
wenzelm
parents: 49614
diff changeset
   202
          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   203
      }
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   204
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   205
    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   206
      : XML.Body =
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   207
    {
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   208
      val body = new mutable.ListBuffer[XML.Tree]
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   209
      var last = elem_range.start
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   210
      for ((range, entry) <- entries) {
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   211
        val subrange = range.restrict(elem_range)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   212
        body ++= make_text(last, subrange.start)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   213
        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   214
        last = subrange.stop
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   215
      }
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   216
      body ++= make_text(last, elem_range.stop)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   217
      make_elems(elem_markup, body.toList)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   218
    }
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   219
   make_body(root_range, Nil, overlapping(root_range))
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   220
  }
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   221
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   222
  def to_XML(text: CharSequence): XML.Body =
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   223
    to_XML(Text.Range(0, text.length), text, (_: XML.Elem) => true)
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   224
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   225
  def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   226
    result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   227
  {
50551
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   228
    val notable: Elements => Boolean =
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   229
      result_elements match {
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   230
        case Some(res) => (elements: Elements) => res.exists(elements.contains)
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   231
        case None => (elements: Elements) => true
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   232
      }
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
   233
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   234
    def results(x: A, entry: Entry): Option[A] =
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   235
    {
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   236
      var y = x
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   237
      var changed = false
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   238
      for {
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   239
        info <- entry.rev_markup // FIXME proper cumulation order (including status markup) (!?)
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   240
        y1 <- result(y, Text.Info(entry.range, info))
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   241
      } { y = y1; changed = true }
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   242
      if (changed) Some(y) else None
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   243
    }
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   244
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   245
    def traverse(
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   246
      last: Text.Offset,
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   247
      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   248
    {
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   249
      stack match {
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   250
        case (parent, (range, entry) :: more) :: rest =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   251
          val subrange = range.restrict(root_range)
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   252
          val subtree =
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   253
            if (notable(entry.subtree_elements))
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   254
              entry.subtree.overlapping(subrange).toList
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   255
            else Nil
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   256
          val start = subrange.start
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   257
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   258
          (if (notable(entry.elements)) results(parent.info, entry) else None) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   259
            case Some(res) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   260
              val next = Text.Info(subrange, res)
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   261
              val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   262
              if (last < start) parent.restrict(Text.Range(last, start)) :: nexts
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   263
              else nexts
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   264
            case None => traverse(last, (parent, subtree ::: more) :: rest)
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   265
          }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   266
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   267
        case (parent, Nil) :: rest =>
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   268
          val stop = parent.range.stop
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   269
          val nexts = traverse(stop, rest)
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   270
          if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   271
          else nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   272
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   273
        case Nil =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   274
          val stop = root_range.stop
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   275
          if (last < stop) List(Text.Info(Text.Range(last, stop), root_info))
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   276
          else Nil
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   277
      }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   278
    }
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   279
    traverse(root_range.start,
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   280
      List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   281
  }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   282
}
34514
2104a836b415 renamed fields of MarkupNode; implemented flatten and leafs
immler@in.tum.de
parents: 34503
diff changeset
   283