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);
authorwenzelm
Thu Mar 27 20:28:19 2014 +0100 (2014-03-27)
changeset 563072bdf8261677a
parent 56306 0fc032898b05
child 56308 ebd3bf053969
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);
src/Pure/PIDE/markup_tree.scala
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 19:47:30 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 20:28:19 2014 +0100
     1.3 @@ -116,10 +116,6 @@
     1.4    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     1.5      this(branches + (entry.range -> entry))
     1.6  
     1.7 -  def overlaps(range: Text.Range): Boolean =
     1.8 -    !branches.isEmpty &&
     1.9 -    Text.Range(branches.firstKey.start, branches.lastKey.stop).overlaps(range)
    1.10 -
    1.11    private def overlapping(range: Text.Range): Branches.T =
    1.12    {
    1.13      val start = Text.Range(range.start)
    1.14 @@ -131,6 +127,11 @@
    1.15      }
    1.16    }
    1.17  
    1.18 +  def restrict(range: Text.Range): Markup_Tree =
    1.19 +    new Markup_Tree(overlapping(range))
    1.20 +
    1.21 +  def is_empty: Boolean = branches.isEmpty
    1.22 +
    1.23    def + (new_markup: Text.Markup): Markup_Tree =
    1.24    {
    1.25      val new_range = new_markup.range
    1.26 @@ -160,18 +161,21 @@
    1.27    def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
    1.28    {
    1.29      def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
    1.30 -      if (tree1.eq(tree2) || !tree2.overlaps(root_range)) tree1
    1.31 -      else
    1.32 -        (tree1 /: tree2.branches)(
    1.33 -          { case (tree, (range, entry)) =>
    1.34 -              if (!range.overlaps(root_range)) tree
    1.35 -              else
    1.36 -                (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
    1.37 -                  { case (t, elem) => t + Text.Info(range, elem) })
    1.38 -          })
    1.39 +      (tree1 /: tree2.branches)(
    1.40 +        { case (tree, (range, entry)) =>
    1.41 +            if (!range.overlaps(root_range)) tree
    1.42 +            else
    1.43 +              (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
    1.44 +                { case (t, elem) => t + Text.Info(range, elem) })
    1.45 +        })
    1.46  
    1.47 -    if (!this.overlaps(root_range)) other
    1.48 -    else merge_trees(this, other)
    1.49 +    if (this eq other) this
    1.50 +    else {
    1.51 +      val tree1 = this.restrict(root_range)
    1.52 +      val tree2 = other.restrict(root_range)
    1.53 +      if (tree1.is_empty) tree2
    1.54 +      else merge_trees(tree1, tree2)
    1.55 +    }
    1.56    }
    1.57  
    1.58    def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,