--- a/src/Pure/PIDE/command.scala Wed Mar 26 21:01:09 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Mar 27 10:43:43 2014 +0100
@@ -27,8 +27,8 @@
{
type Entry = (Long, XML.Tree)
val empty = new Results(SortedMap.empty)
- def make(es: Iterable[Results.Entry]): Results = (empty /: es.iterator)(_ + _)
- def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
+ def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
+ def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
}
final class Results private(private val rep: SortedMap[Long, XML.Tree])
@@ -98,6 +98,15 @@
/* state */
+ object State
+ {
+ 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)))
+ }
+
sealed case class State(
command: Command,
status: List[Markup] = Nil,
@@ -108,9 +117,6 @@
def markup(index: Markup_Index): Markup_Tree = markups(index)
- def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
- markup(Markup_Index.markup).to_XML(command.range, command.source, filter)
-
/* content */