src/Pure/PIDE/text.scala
changeset 44474 681447a9ffe5
parent 44473 4f264fdf8d0e
child 45240 9d97bd3c086a
equal deleted inserted replaced
44473:4f264fdf8d0e 44474:681447a9ffe5
    62 
    62 
    63   /* perspective */
    63   /* perspective */
    64 
    64 
    65   object Perspective
    65   object Perspective
    66   {
    66   {
    67     val empty = Perspective(Nil)
    67     val empty: Perspective = Perspective(Nil)
    68 
    68 
    69     def apply(ranges: Seq[Range]): Perspective =
    69     def apply(ranges: Seq[Range]): Perspective =
    70     {
    70     {
    71       val sorted_ranges = ranges.toArray
    71       val sorted_ranges = ranges.toArray
    72       Sorting.quickSort(sorted_ranges)(Range.Ordering)
    72       Sorting.quickSort(sorted_ranges)(Range.Ordering)