--- a/src/Pure/PIDE/command.scala Mon Dec 01 13:49:47 2014 +0100
+++ b/src/Pure/PIDE/command.scala Mon Dec 01 14:24:05 2014 +0100
@@ -27,8 +27,8 @@
{
type Entry = (Long, XML.Tree)
val empty = new Results(SortedMap.empty)
- def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
- def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
+ def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
+ def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
}
final class Results private(private val rep: SortedMap[Long, XML.Tree])