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