more frugal merge of markup trees: filter wrt. subsequent query;
authorwenzelm
Thu Mar 27 12:11:32 2014 +0100 (2014-03-27)
changeset 563011da7b4c33db9
parent 56300 8346b664fa7a
child 56302 c63ab5263008
more frugal merge of markup trees: filter wrt. subsequent query;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Mar 27 11:19:31 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Mar 27 12:11:32 2014 +0100
     1.3 @@ -81,11 +81,6 @@
     1.4      def add(index: Markup_Index, markup: Text.Markup): Markups =
     1.5        new Markups(rep + (index -> (this(index) + markup)))
     1.6  
     1.7 -    def ++ (other: Markups): Markups =
     1.8 -      new Markups(
     1.9 -        (rep.keySet ++ other.rep.keySet)
    1.10 -          .map(index => index -> (this(index) ++ other(index))).toMap)
    1.11 -
    1.12      override def hashCode: Int = rep.hashCode
    1.13      override def equals(that: Any): Boolean =
    1.14        that match {
    1.15 @@ -103,8 +98,9 @@
    1.16      def merge_results(states: List[State]): Command.Results =
    1.17        Results.merge(states.map(_.results))
    1.18  
    1.19 -    def merge_markup(states: List[State], index: Markup_Index): Markup_Tree =
    1.20 -      Markup_Tree.merge(states.map(_.markup(index)))
    1.21 +    def merge_markup(states: List[State], index: Markup_Index,
    1.22 +        range: Text.Range, elements: Document.Elements): Markup_Tree =
    1.23 +      Markup_Tree.merge(states.map(_.markup(index)), range, elements)
    1.24    }
    1.25  
    1.26    sealed case class State(
    1.27 @@ -203,13 +199,6 @@
    1.28                this
    1.29            }
    1.30      }
    1.31 -
    1.32 -    def ++ (other: State): State =
    1.33 -      copy(
    1.34 -        status = other.status ::: status,
    1.35 -        results = results ++ other.results,
    1.36 -        markups = markups ++ other.markups
    1.37 -      )
    1.38    }
    1.39  
    1.40  
     2.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 27 11:19:31 2014 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 27 12:11:32 2014 +0100
     2.3 @@ -650,13 +650,15 @@
     2.4      def command_results(version: Version, command: Command): Command.Results =
     2.5        Command.State.merge_results(command_states(version, command))
     2.6  
     2.7 -    def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
     2.8 -      Command.State.merge_markup(command_states(version, command), index)
     2.9 +    def command_markup(version: Version, command: Command, index: Command.Markup_Index,
    2.10 +        range: Text.Range, elements: Elements): Markup_Tree =
    2.11 +      Command.State.merge_markup(command_states(version, command), index, range, elements)
    2.12  
    2.13      def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
    2.14        (for {
    2.15          command <- node.commands.iterator
    2.16 -        markup = command_markup(version, command, Command.Markup_Index.markup)
    2.17 +        markup =
    2.18 +          command_markup(version, command, Command.Markup_Index.markup, command.range, elements)
    2.19          tree <- markup.to_XML(command.range, command.source, elements)
    2.20        } yield tree).toList
    2.21  
    2.22 @@ -734,8 +736,9 @@
    2.23                  chunk <- thy_load_command.chunks.get(file_name).iterator
    2.24                  states = state.command_states(version, thy_load_command)
    2.25                  res = result(Command.State.merge_results(states))
    2.26 -                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    2.27 -                  former_range.restrict(chunk.range), info, elements,
    2.28 +                range = former_range.restrict(chunk.range)
    2.29 +                markup = Command.State.merge_markup(states, markup_index, range, elements)
    2.30 +                Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    2.31                    { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
    2.32                  ).iterator
    2.33                } yield Text.Info(convert(r0), a)).toList
    2.34 @@ -746,8 +749,9 @@
    2.35                  (command, command_start) <- node.command_range(former_range)
    2.36                  states = state.command_states(version, command)
    2.37                  res = result(Command.State.merge_results(states))
    2.38 -                Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
    2.39 -                  (former_range - command_start).restrict(command.range), info, elements,
    2.40 +                range = (former_range - command_start).restrict(command.range)
    2.41 +                markup = Command.State.merge_markup(states, markup_index, range, elements)
    2.42 +                Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
    2.43                    {
    2.44                      case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
    2.45                    }).iterator
     3.1 --- a/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 11:19:31 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup_tree.scala	Thu Mar 27 12:11:32 2014 +0100
     3.3 @@ -20,8 +20,8 @@
     3.4  
     3.5    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
     3.6  
     3.7 -  def merge(trees: List[Markup_Tree]): Markup_Tree =
     3.8 -    (empty /: trees)(_ ++ _)
     3.9 +  def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
    3.10 +    (empty /: trees)(_.merge(_, range, elements))
    3.11  
    3.12    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    3.13      trees match {
    3.14 @@ -116,12 +116,6 @@
    3.15    private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
    3.16      this(branches + (entry.range -> entry))
    3.17  
    3.18 -  override def toString =
    3.19 -    branches.toList.map(_._2) match {
    3.20 -      case Nil => "Empty"
    3.21 -      case list => list.mkString("Tree(", ",", ")")
    3.22 -    }
    3.23 -
    3.24    private def overlapping(range: Text.Range): Branches.T =
    3.25    {
    3.26      val start = Text.Range(range.start)
    3.27 @@ -159,43 +153,22 @@
    3.28      }
    3.29    }
    3.30  
    3.31 -  def ++ (other: Markup_Tree): Markup_Tree =
    3.32 -    if (this eq other) this
    3.33 -    else if (branches.isEmpty) other
    3.34 -    else
    3.35 -      (this /: other.branches)({ case (tree, (range, entry)) =>
    3.36 -        ((tree ++ entry.subtree) /: entry.markup)(
    3.37 -          { case (t, elem) => t + Text.Info(range, elem) }) })
    3.38 -
    3.39 -  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
    3.40 +  def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
    3.41    {
    3.42 -    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    3.43 -      if (start == stop) Nil
    3.44 -      else List(XML.Text(text.subSequence(start, stop).toString))
    3.45 +    def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
    3.46 +      if (tree1 eq tree2) tree1
    3.47 +      else if (tree1.branches.isEmpty) tree2
    3.48 +      else
    3.49 +        (tree1 /: tree2.branches)(
    3.50 +          { case (tree, (range, entry)) =>
    3.51 +              if (range overlaps root_range) {
    3.52 +                (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
    3.53 +                  { case (t, elem) => t + Text.Info(range, elem) })
    3.54 +              }
    3.55 +              else tree
    3.56 +          })
    3.57  
    3.58 -    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    3.59 -      (body /: rev_markups) {
    3.60 -        case (b, elem) =>
    3.61 -          if (!elements(elem.name)) b
    3.62 -          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
    3.63 -          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
    3.64 -      }
    3.65 -
    3.66 -    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
    3.67 -      : XML.Body =
    3.68 -    {
    3.69 -      val body = new mutable.ListBuffer[XML.Tree]
    3.70 -      var last = elem_range.start
    3.71 -      for ((range, entry) <- entries) {
    3.72 -        val subrange = range.restrict(elem_range)
    3.73 -        body ++= make_text(last, subrange.start)
    3.74 -        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
    3.75 -        last = subrange.stop
    3.76 -      }
    3.77 -      body ++= make_text(last, elem_range.stop)
    3.78 -      make_elems(elem_markup, body.toList)
    3.79 -    }
    3.80 -   make_body(root_range, Nil, overlapping(root_range))
    3.81 +    merge_trees(this, other)
    3.82    }
    3.83  
    3.84    def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
    3.85 @@ -246,5 +219,42 @@
    3.86      traverse(root_range.start,
    3.87        List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
    3.88    }
    3.89 +
    3.90 +  def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
    3.91 +  {
    3.92 +    def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
    3.93 +      if (start == stop) Nil
    3.94 +      else List(XML.Text(text.subSequence(start, stop).toString))
    3.95 +
    3.96 +    def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
    3.97 +      (body /: rev_markups) {
    3.98 +        case (b, elem) =>
    3.99 +          if (!elements(elem.name)) b
   3.100 +          else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
   3.101 +          else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
   3.102 +      }
   3.103 +
   3.104 +    def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
   3.105 +      : XML.Body =
   3.106 +    {
   3.107 +      val body = new mutable.ListBuffer[XML.Tree]
   3.108 +      var last = elem_range.start
   3.109 +      for ((range, entry) <- entries) {
   3.110 +        val subrange = range.restrict(elem_range)
   3.111 +        body ++= make_text(last, subrange.start)
   3.112 +        body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
   3.113 +        last = subrange.stop
   3.114 +      }
   3.115 +      body ++= make_text(last, elem_range.stop)
   3.116 +      make_elems(elem_markup, body.toList)
   3.117 +    }
   3.118 +   make_body(root_range, Nil, overlapping(root_range))
   3.119 +  }
   3.120 +
   3.121 +  override def toString =
   3.122 +    branches.toList.map(_._2) match {
   3.123 +      case Nil => "Empty"
   3.124 +      case list => list.mkString("Tree(", ",", ")")
   3.125 +    }
   3.126  }
   3.127  
     4.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 27 11:19:31 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Mar 27 12:11:32 2014 +0100
     4.3 @@ -160,7 +160,9 @@
     4.4          val root = data.root
     4.5          for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
     4.6            val markup =
     4.7 -            snapshot.state.command_markup(snapshot.version, command, Command.Markup_Index.markup)
     4.8 +            snapshot.state.command_markup(
     4.9 +              snapshot.version, command, Command.Markup_Index.markup,
    4.10 +                command.range, Document.Elements.full)
    4.11            Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
    4.12                {
    4.13                  val range = info.range + command_start