more frugal merge of markup trees: filter wrt. subsequent query;
--- a/src/Pure/PIDE/command.scala Thu Mar 27 11:19:31 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Mar 27 12:11:32 2014 +0100
@@ -81,11 +81,6 @@
def add(index: Markup_Index, markup: Text.Markup): Markups =
new Markups(rep + (index -> (this(index) + markup)))
- def ++ (other: Markups): Markups =
- new Markups(
- (rep.keySet ++ other.rep.keySet)
- .map(index => index -> (this(index) ++ other(index))).toMap)
-
override def hashCode: Int = rep.hashCode
override def equals(that: Any): Boolean =
that match {
@@ -103,8 +98,9 @@
def merge_results(states: List[State]): Command.Results =
Results.merge(states.map(_.results))
- def merge_markup(states: List[State], index: Markup_Index): Markup_Tree =
- Markup_Tree.merge(states.map(_.markup(index)))
+ def merge_markup(states: List[State], index: Markup_Index,
+ range: Text.Range, elements: Document.Elements): Markup_Tree =
+ Markup_Tree.merge(states.map(_.markup(index)), range, elements)
}
sealed case class State(
@@ -203,13 +199,6 @@
this
}
}
-
- def ++ (other: State): State =
- copy(
- status = other.status ::: status,
- results = results ++ other.results,
- markups = markups ++ other.markups
- )
}
--- a/src/Pure/PIDE/document.scala Thu Mar 27 11:19:31 2014 +0100
+++ b/src/Pure/PIDE/document.scala Thu Mar 27 12:11:32 2014 +0100
@@ -650,13 +650,15 @@
def command_results(version: Version, command: Command): Command.Results =
Command.State.merge_results(command_states(version, command))
- def command_markup(version: Version, command: Command, index: Command.Markup_Index): Markup_Tree =
- Command.State.merge_markup(command_states(version, command), index)
+ def command_markup(version: Version, command: Command, index: Command.Markup_Index,
+ range: Text.Range, elements: Elements): Markup_Tree =
+ Command.State.merge_markup(command_states(version, command), index, range, elements)
def markup_to_XML(version: Version, node: Node, elements: Elements): XML.Body =
(for {
command <- node.commands.iterator
- markup = command_markup(version, command, Command.Markup_Index.markup)
+ markup =
+ command_markup(version, command, Command.Markup_Index.markup, command.range, elements)
tree <- markup.to_XML(command.range, command.source, elements)
} yield tree).toList
@@ -734,8 +736,9 @@
chunk <- thy_load_command.chunks.get(file_name).iterator
states = state.command_states(version, thy_load_command)
res = result(Command.State.merge_results(states))
- Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
- former_range.restrict(chunk.range), info, elements,
+ range = former_range.restrict(chunk.range)
+ markup = Command.State.merge_markup(states, markup_index, range, elements)
+ Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
{ case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
).iterator
} yield Text.Info(convert(r0), a)).toList
@@ -746,8 +749,9 @@
(command, command_start) <- node.command_range(former_range)
states = state.command_states(version, command)
res = result(Command.State.merge_results(states))
- Text.Info(r0, a) <- Command.State.merge_markup(states, markup_index).cumulate[A](
- (former_range - command_start).restrict(command.range), info, elements,
+ range = (former_range - command_start).restrict(command.range)
+ markup = Command.State.merge_markup(states, markup_index, range, elements)
+ Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
{
case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0 + command_start), b))
}).iterator
--- a/src/Pure/PIDE/markup_tree.scala Thu Mar 27 11:19:31 2014 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Thu Mar 27 12:11:32 2014 +0100
@@ -20,8 +20,8 @@
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
- def merge(trees: List[Markup_Tree]): Markup_Tree =
- (empty /: trees)(_ ++ _)
+ def merge(trees: List[Markup_Tree], range: Text.Range, elements: Document.Elements): Markup_Tree =
+ (empty /: trees)(_.merge(_, range, elements))
def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
trees match {
@@ -116,12 +116,6 @@
private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
this(branches + (entry.range -> entry))
- override def toString =
- branches.toList.map(_._2) match {
- case Nil => "Empty"
- case list => list.mkString("Tree(", ",", ")")
- }
-
private def overlapping(range: Text.Range): Branches.T =
{
val start = Text.Range(range.start)
@@ -159,43 +153,22 @@
}
}
- def ++ (other: Markup_Tree): Markup_Tree =
- if (this eq other) this
- else if (branches.isEmpty) other
- else
- (this /: other.branches)({ case (tree, (range, entry)) =>
- ((tree ++ entry.subtree) /: entry.markup)(
- { case (t, elem) => t + Text.Info(range, elem) }) })
-
- def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+ def merge(other: Markup_Tree, root_range: Text.Range, elements: Document.Elements): Markup_Tree =
{
- def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
- if (start == stop) Nil
- else List(XML.Text(text.subSequence(start, stop).toString))
+ def merge_trees(tree1: Markup_Tree, tree2: Markup_Tree): Markup_Tree =
+ if (tree1 eq tree2) tree1
+ else if (tree1.branches.isEmpty) tree2
+ else
+ (tree1 /: tree2.branches)(
+ { case (tree, (range, entry)) =>
+ if (range overlaps root_range) {
+ (merge_trees(tree, entry.subtree) /: entry.filter_markup(elements))(
+ { case (t, elem) => t + Text.Info(range, elem) })
+ }
+ else tree
+ })
- def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
- (body /: rev_markups) {
- case (b, elem) =>
- if (!elements(elem.name)) b
- else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
- else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
- }
-
- def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
- : XML.Body =
- {
- val body = new mutable.ListBuffer[XML.Tree]
- var last = elem_range.start
- for ((range, entry) <- entries) {
- val subrange = range.restrict(elem_range)
- body ++= make_text(last, subrange.start)
- body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
- last = subrange.stop
- }
- body ++= make_text(last, elem_range.stop)
- make_elems(elem_markup, body.toList)
- }
- make_body(root_range, Nil, overlapping(root_range))
+ merge_trees(this, other)
}
def cumulate[A](root_range: Text.Range, root_info: A, elements: Document.Elements,
@@ -246,5 +219,42 @@
traverse(root_range.start,
List((Text.Info(root_range, root_info), overlapping(root_range).toList)))
}
+
+ def to_XML(root_range: Text.Range, text: CharSequence, elements: Document.Elements): XML.Body =
+ {
+ def make_text(start: Text.Offset, stop: Text.Offset): XML.Body =
+ if (start == stop) Nil
+ else List(XML.Text(text.subSequence(start, stop).toString))
+
+ def make_elems(rev_markups: List[XML.Elem], body: XML.Body): XML.Body =
+ (body /: rev_markups) {
+ case (b, elem) =>
+ if (!elements(elem.name)) b
+ else if (elem.body.isEmpty) List(XML.Elem(elem.markup, b))
+ else List(XML.Wrapped_Elem(elem.markup, elem.body, b))
+ }
+
+ def make_body(elem_range: Text.Range, elem_markup: List[XML.Elem], entries: Branches.T)
+ : XML.Body =
+ {
+ val body = new mutable.ListBuffer[XML.Tree]
+ var last = elem_range.start
+ for ((range, entry) <- entries) {
+ val subrange = range.restrict(elem_range)
+ body ++= make_text(last, subrange.start)
+ body ++= make_body(subrange, entry.rev_markup, entry.subtree.overlapping(subrange))
+ last = subrange.stop
+ }
+ body ++= make_text(last, elem_range.stop)
+ make_elems(elem_markup, body.toList)
+ }
+ make_body(root_range, Nil, overlapping(root_range))
+ }
+
+ override def toString =
+ branches.toList.map(_._2) match {
+ case Nil => "Empty"
+ case list => list.mkString("Tree(", ",", ")")
+ }
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 27 11:19:31 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Mar 27 12:11:32 2014 +0100
@@ -160,7 +160,9 @@
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
val markup =
- snapshot.state.command_markup(snapshot.version, command, Command.Markup_Index.markup)
+ snapshot.state.command_markup(
+ snapshot.version, command, Command.Markup_Index.markup,
+ command.range, Document.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, root, (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start