# HG changeset patch # User wenzelm # Date 1395918692 -3600 # Node ID 1da7b4c33db970443ce6eae32e0a06d70b1d64f8 # Parent 8346b664fa7a59a0b88e9a6f25fb9264c43f4ac1 more frugal merge of markup trees: filter wrt. subsequent query; diff -r 8346b664fa7a -r 1da7b4c33db9 src/Pure/PIDE/command.scala --- 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 - ) } diff -r 8346b664fa7a -r 1da7b4c33db9 src/Pure/PIDE/document.scala --- 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 diff -r 8346b664fa7a -r 1da7b4c33db9 src/Pure/PIDE/markup_tree.scala --- 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(", ",", ")") + } } diff -r 8346b664fa7a -r 1da7b4c33db9 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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