tuned signature;
authorwenzelm
Mon Dec 01 14:24:05 2014 +0100 (2014-12-01 ago)
changeset 5907227c6936c6484
parent 59071 4af6060734d5
child 59073 dcecfcc56dce
tuned signature;
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Mon Dec 01 13:49:47 2014 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Dec 01 14:24:05 2014 +0100
     1.3 @@ -27,8 +27,8 @@
     1.4    {
     1.5      type Entry = (Long, XML.Tree)
     1.6      val empty = new Results(SortedMap.empty)
     1.7 -    def make(es: List[Results.Entry]): Results = (empty /: es)(_ + _)
     1.8 -    def merge(rs: List[Results]): Results = (empty /: rs)(_ ++ _)
     1.9 +    def make(args: TraversableOnce[Results.Entry]): Results = (empty /: args)(_ + _)
    1.10 +    def merge(args: TraversableOnce[Results]): Results = (empty /: args)(_ ++ _)
    1.11    }
    1.12  
    1.13    final class Results private(private val rep: SortedMap[Long, XML.Tree])