tuned signature;
authorwenzelm
Mon, 01 Dec 2014 14:24:05 +0100
changeset 59072 27c6936c6484
parent 59071 4af6060734d5
child 59073 dcecfcc56dce
tuned signature;
src/Pure/PIDE/command.scala
--- 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])