src/Pure/PIDE/markup_tree.scala
author wenzelm
Sun, 10 Jan 2021 13:04:29 +0100
changeset 73120 c3589f2dff31
parent 72815 85aaaf2cd173
child 73359 d8a0e996614b
permissions -rw-r--r--
more informative errors: simplify diagnosis of spurious failures reported by users;
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
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    11
import scala.collection.immutable.SortedMap
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
    12
import scala.collection.mutable
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    13
import scala.annotation.tailrec
38479
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
{
50551
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    18
  /* construct trees */
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    19
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    20
  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
    21
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56313
diff changeset
    22
  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Markup.Elements): Markup_Tree =
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
    23
    (empty /: trees)(_.merge(_, range, elements))
56299
8201790fdeb9 more careful treatment of multiple command states (eval + prints): merge content that is actually required;
wenzelm
parents: 55820
diff changeset
    24
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    25
  def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    26
    trees match {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    27
      case Nil => empty
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    28
      case head :: tail =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    29
        new Markup_Tree(
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    30
          (head.branches /: tail) {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    31
            case (branches, tree) =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    32
              (branches /: tree.branches) {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    33
                case (bs, (r, entry)) =>
73120
c3589f2dff31 more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents: 72815
diff changeset
    34
                  require(!bs.isDefinedAt(r), "cannot merge markup trees")
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    35
                  bs + (r -> entry)
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
          })
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    38
    }
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    39
50551
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
  /* tree building blocks */
67d934cdc9b9 more formal class Markup_Tree.Elements;
wenzelm
parents: 49650
diff changeset
    42
45473
wenzelm
parents: 45470
diff changeset
    43
  object Entry
wenzelm
parents: 45470
diff changeset
    44
  {
wenzelm
parents: 45470
diff changeset
    45
    def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
55652
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
    46
      Entry(markup.range, List(markup.info), subtree)
45473
wenzelm
parents: 45470
diff changeset
    47
  }
wenzelm
parents: 45470
diff changeset
    48
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    49
  sealed case class Entry(
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    50
    range: Text.Range,
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    51
    rev_markup: List[XML.Elem],
55652
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
    52
    subtree: Markup_Tree)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    53
  {
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
    54
    def markup: List[XML.Elem] = rev_markup.reverse
45474
f793dd5d84b2 index markup elements for more efficient cumulate/select operations;
wenzelm
parents: 45473
diff changeset
    55
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56313
diff changeset
    56
    def filter_markup(elements: Markup.Elements): List[XML.Elem] =
55645
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
    57
    {
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
    58
      var result: List[XML.Elem] = Nil
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 58463
diff changeset
    59
      for (elem <- rev_markup if elements(elem.name))
55645
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
    60
        result ::= elem
72815
wenzelm
parents: 71383
diff changeset
    61
      result
55645
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
    62
    }
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
    63
55652
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
    64
    def + (markup: Text.Markup): Entry = copy(rev_markup = markup.info :: rev_markup)
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
    65
    def \ (markup: Text.Markup): Entry = copy(subtree = subtree + markup)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    66
  }
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
    67
38479
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    68
  object Branches
e628da370072 more efficient Markup_Tree, based on branches sorted by quasi-order;
wenzelm
parents: 38478
diff changeset
    69
  {
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
    70
    type T = SortedMap[Text.Range, Entry]
45456
9ba615ac75fb more abstract Markup_Tree;
wenzelm
parents: 45455
diff changeset
    71
    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
    72
  }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    73
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    74
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    75
  /* XML representation */
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    76
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
    77
  @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
    78
      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
    79
    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
    80
      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
    81
        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
    82
      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
    83
        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
    84
      case _ => (elems, body)
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    85
    }
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    86
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    87
  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
    88
    {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    89
      val (offset, markup_trees) = acc
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    90
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    91
      strip_elems(Nil, List(tree)) match {
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    92
        case (Nil, body) =>
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
    93
          (offset + XML.text_length(body), markup_trees)
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
    94
49469
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
    95
        case (elems, body) =>
00c301c8d569 more direct Markup_Tree.from_XML;
wenzelm
parents: 49467
diff changeset
    96
          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
    97
          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
    98
          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
    99
            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
   100
            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
   101
            (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
   102
          }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
   103
      }
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   104
    }
49466
99ed1f422635 tuned signature;
wenzelm
parents: 49465
diff changeset
   105
49467
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   106
  def from_XML(body: XML.Body): Markup_Tree =
25b7e843e124 more direct Markup_Tree.from_XML;
wenzelm
parents: 49466
diff changeset
   107
    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
   108
}
34554
7dc6c231da40 abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents: 34517
diff changeset
   109
34393
f0e1608a774f basic tree structure for sidekick
immler@in.tum.de
parents:
diff changeset
   110
51618
a3577cd80c41 tuned signature -- avoid intrusion of slightly odd Swing structures into pure Markup_Tree;
wenzelm
parents: 50642
diff changeset
   111
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
   112
{
49417
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
   113
  import Markup_Tree._
c5a8592fb5d3 recover order of stacked markup;
wenzelm
parents: 48762
diff changeset
   114
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   115
  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
   116
    this(branches + (entry.range -> entry))
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   117
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   118
  private def overlapping(range: Text.Range): Branches.T =
56311
wenzelm
parents: 56307
diff changeset
   119
    if (branches.isEmpty ||
56313
84d047625f70 tuned -- see Text.Range.overlaps(Range);
wenzelm
parents: 56311
diff changeset
   120
        (range.contains(branches.firstKey.start) && branches.lastKey.stop <= range.stop))
56311
wenzelm
parents: 56307
diff changeset
   121
      branches
wenzelm
parents: 56307
diff changeset
   122
    else {
wenzelm
parents: 56307
diff changeset
   123
      val start = Text.Range(range.start)
wenzelm
parents: 56307
diff changeset
   124
      val stop = Text.Range(range.stop)
wenzelm
parents: 56307
diff changeset
   125
      val bs = branches.range(start, stop)
wenzelm
parents: 56307
diff changeset
   126
      branches.get(stop) match {
wenzelm
parents: 56307
diff changeset
   127
        case Some(end) if range overlaps end.range => bs + (end.range -> end)
wenzelm
parents: 56307
diff changeset
   128
        case _ => bs
wenzelm
parents: 56307
diff changeset
   129
      }
45457
wenzelm
parents: 45456
diff changeset
   130
    }
wenzelm
parents: 45456
diff changeset
   131
56307
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   132
  def restrict(range: Text.Range): Markup_Tree =
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   133
    new Markup_Tree(overlapping(range))
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   134
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   135
  def is_empty: Boolean = branches.isEmpty
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   136
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   137
  def + (new_markup: Text.Markup): Markup_Tree =
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   138
  {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   139
    val new_range = new_markup.range
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   140
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
   141
    branches.get(new_range) match {
45473
wenzelm
parents: 45470
diff changeset
   142
      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
   143
      case Some(entry) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   144
        if (entry.range == new_range)
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   145
          new Markup_Tree(branches, entry + new_markup)
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   146
        else if (entry.range.contains(new_range))
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   147
          new Markup_Tree(branches, entry \ new_markup)
38578
1ebc6b76e5ff misc tuning and simplification;
wenzelm
parents: 38577
diff changeset
   148
        else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
45473
wenzelm
parents: 45470
diff changeset
   149
          new Markup_Tree(Branches.empty, Entry(new_markup, this))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   150
        else {
45457
wenzelm
parents: 45456
diff changeset
   151
          val body = overlapping(new_range)
49607
b610c0d52bfa updated to consolidated SortedMap in scala-2.9.x;
wenzelm
parents: 49469
diff changeset
   152
          if (body.forall(e => new_range.contains(e._1)))
b610c0d52bfa updated to consolidated SortedMap in scala-2.9.x;
wenzelm
parents: 49469
diff changeset
   153
            new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
49608
wenzelm
parents: 49607
diff changeset
   154
          else {
58463
0bf0e9788d54 tuned message;
wenzelm
parents: 57912
diff changeset
   155
            Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
71383
8313dca6dee9 misc tuning, following hint by IntelliJ;
wenzelm
parents: 64370
diff changeset
   156
              body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
38482
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   157
            this
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   158
          }
7b6ee937b75f tuned Markup_Tree, using SortedMap more carefully;
wenzelm
parents: 38479
diff changeset
   159
        }
34703
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   160
    }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   161
  }
ff037c17332a minor tuning;
wenzelm
parents: 34701
diff changeset
   162
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56313
diff changeset
   163
  def merge(other: Markup_Tree, root_range: Text.Range, elements: Markup.Elements): Markup_Tree =
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   164
  {
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   165
    def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
56307
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   166
      (tree1 /: tree2.branches)(
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   167
        { case (tree, (range, entry)) =>
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   168
            if (!range.overlaps(root_range)) tree
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   169
            else
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   170
              (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   171
                { case (t, elem) => t + Text.Info(range, elem) })
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   172
        })
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   173
56307
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   174
    if (this eq other) this
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   175
    else {
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   176
      val tree1 = this.restrict(root_range)
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   177
      val tree2 = other.restrict(root_range)
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   178
      if (tree1.is_empty) tree2
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   179
      else merge_trees(tree1, tree2)
2bdf8261677a more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);
wenzelm
parents: 56302
diff changeset
   180
    }
49614
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   181
  }
0009a6ebc83b operations to turn markup into XML;
wenzelm
parents: 49608
diff changeset
   182
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56313
diff changeset
   183
  def cumulate[A](root_range: Text.Range, root_info: A, elements: Markup.Elements,
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   184
    result: (A, Text.Markup) => Option[A]): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   185
  {
46178
1c5c88f6feb5 clarified Isabelle_Rendering vs. physical painting;
wenzelm
parents: 46165
diff changeset
   186
    def results(x: A, entry: Entry): Option[A] =
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   187
    {
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   188
      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
   189
      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
   190
      for {
55645
561754277494 tuned -- remaining rev_markup is rather short after filter;
wenzelm
parents: 55622
diff changeset
   191
        elem <- entry.filter_markup(elements)
55620
19dffae33cde cumulate/select wrt. precise elements guard;
wenzelm
parents: 55618
diff changeset
   192
        y1 <- result(y, Text.Info(entry.range, elem))
52889
ea3338812e67 more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;
wenzelm
parents: 52642
diff changeset
   193
      } { y = y1; changed = true }
50552
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   194
      if (changed) Some(y) else None
2b7fd8c9c4ac maintain subtree_elements for improved performance of cumulate operator;
wenzelm
parents: 50551
diff changeset
   195
    }
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   196
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   197
    def traverse(
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   198
      last: Text.Offset,
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   199
      stack: List[(Text.Info[A], List[(Text.Range, Entry)])]): List[Text.Info[A]] =
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   200
    {
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   201
      stack match {
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   202
        case (parent, (range, entry) :: more) :: rest =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   203
          val subrange = range.restrict(root_range)
55652
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
   204
          val subtree = entry.subtree.overlapping(subrange).toList
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   205
          val start = subrange.start
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   206
55652
33ad12ef79ff eliminated somewhat pointless elements index (see also f793dd5d84b2, 2b7fed8c9c4ac): less memory and more speed (avoid linear "exists" of 19dffae33cde);
wenzelm
parents: 55645
diff changeset
   207
          results(parent.info, entry) match {
45469
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   208
            case Some(res) =>
25306d92f4ad refined Markup_Tree implementation: stacked markup within each entry;
wenzelm
parents: 45468
diff changeset
   209
              val next = Text.Info(subrange, res)
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   210
              val nexts = traverse(start, (next, subtree) :: (parent, more) :: rest)
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   211
              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
   212
              else nexts
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   213
            case None => traverse(last, (parent, subtree ::: more) :: rest)
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   214
          }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   215
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   216
        case (parent, Nil) :: rest =>
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   217
          val stop = parent.range.stop
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   218
          val nexts = traverse(stop, rest)
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   219
          if (last < stop) parent.restrict(Text.Range(last, stop)) :: nexts
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   220
          else nexts
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   221
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   222
        case Nil =>
45467
3f290b6288cf tuned signature;
wenzelm
parents: 45459
diff changeset
   223
          val stop = root_range.stop
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   224
          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
   225
          else Nil
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   226
      }
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   227
    }
52900
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   228
    traverse(root_range.start,
d29bf6db8a2d more elementary list structures for markup tree traversal;
wenzelm
parents: 52889
diff changeset
   229
      List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
45459
a5c1599f664d added markup_cumulate operator;
wenzelm
parents: 45457
diff changeset
   230
  }
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   231
56743
81370dfadb1d tuned signature;
wenzelm
parents: 56313
diff changeset
   232
  def to_XML(root_range: Text.Range, text: CharSequence, elements: Markup.Elements): XML.Body =
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   233
  {
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   234
    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   235
      if (start == stop) Nil
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   236
      else List(XML.Text(text.subSequence(start, stop).toString))
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   237
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   238
    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   239
      (body /: rev_markups) {
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   240
        case (b, elem) =>
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   241
          if (!elements(elem.name)) b
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   242
          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   243
          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   244
      }
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   245
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   246
    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   247
      : XML.Body =
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   248
    {
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   249
      val body = new mutable.ListBuffer[XML.Tree]
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   250
      var last = elem_range.start
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   251
      for ((range, entry) <- entries) {
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   252
        val subrange = range.restrict(elem_range)
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   253
        body ++= make_text(last, subrange.start)
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   254
        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   255
        last = subrange.stop
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   256
      }
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   257
      body ++= make_text(last, elem_range.stop)
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   258
      make_elems(elem_markup, body.toList)
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   259
    }
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   260
   make_body(root_range, Nil, overlapping(root_range))
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   261
  }
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   262
57912
wenzelm
parents: 56782
diff changeset
   263
  override def toString: String =
56301
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   264
    branches.toList.map(_._2) match {
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   265
      case Nil => "Empty"
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   266
      case list => list.mkString("Tree(", ",", ")")
1da7b4c33db9 more frugal merge of markup trees: filter wrt. subsequent query;
wenzelm
parents: 56300
diff changeset
   267
    }
34717
3f32e08bbb6c sidekick root data: set buffer length to avoid crash of initial caret move;
wenzelm
parents: 34708
diff changeset
   268
}