src/Pure/PIDE/text.scala
changeset 65374 ce09e947c1d5
parent 65196 e8760a98db78
child 65522 4d7c5df70a14
     1.1 --- a/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:47 2017 +0200
     1.2 +++ b/src/Pure/PIDE/text.scala	Tue Apr 04 18:43:58 2017 +0200
     1.3 @@ -82,7 +82,7 @@
     1.4  
     1.5      def full: Perspective = Perspective(List(Range.full))
     1.6  
     1.7 -    def apply(ranges: Seq[Range]): Perspective =
     1.8 +    def apply(ranges: List[Range]): Perspective =
     1.9      {
    1.10        val result = new mutable.ListBuffer[Range]
    1.11        var last: Option[Range] = None