src/Pure/PIDE/text.scala
changeset 44473 4f264fdf8d0e
parent 44384 8f6054a63f96
child 44474 681447a9ffe5
equal deleted inserted replaced
44472:6f2943e34d60 44473:4f264fdf8d0e
    60   }
    60   }
    61 
    61 
    62 
    62 
    63   /* perspective */
    63   /* perspective */
    64 
    64 
    65   type Perspective = List[Range]  // visible text partitioning in canonical order
    65   object Perspective
       
    66   {
       
    67     val empty = Perspective(Nil)
    66 
    68 
    67   def perspective(ranges: Seq[Range]): Perspective =
    69     def apply(ranges: Seq[Range]): Perspective =
       
    70     {
       
    71       val sorted_ranges = ranges.toArray
       
    72       Sorting.quickSort(sorted_ranges)(Range.Ordering)
       
    73 
       
    74       val result = new mutable.ListBuffer[Text.Range]
       
    75       var last: Option[Text.Range] = None
       
    76       for (range <- sorted_ranges)
       
    77       {
       
    78         last match {
       
    79           case Some(last_range)
       
    80           if ((last_range overlaps range) || last_range.stop == range.start) =>
       
    81             last = Some(Text.Range(last_range.start, range.stop))
       
    82           case _ =>
       
    83             result ++= last
       
    84             last = Some(range)
       
    85         }
       
    86       }
       
    87       result ++= last
       
    88       new Perspective(result.toList)
       
    89     }
       
    90   }
       
    91 
       
    92   sealed case class Perspective(ranges: List[Range]) // visible text partitioning in canonical order
    68   {
    93   {
    69     val sorted_ranges = ranges.toArray
    94     def is_empty: Boolean = ranges.isEmpty
    70     Sorting.quickSort(sorted_ranges)(Range.Ordering)
    95     def range: Range =
    71 
    96       if (is_empty) Range(0)
    72     val result = new mutable.ListBuffer[Text.Range]
    97       else Range(ranges.head.start, ranges.last.stop)
    73     var last: Option[Text.Range] = None
       
    74     for (range <- sorted_ranges)
       
    75     {
       
    76       last match {
       
    77         case Some(last_range)
       
    78         if ((last_range overlaps range) || last_range.stop == range.start) =>
       
    79           last = Some(Text.Range(last_range.start, range.stop))
       
    80         case _ =>
       
    81           result ++= last
       
    82           last = Some(range)
       
    83       }
       
    84     }
       
    85     result ++= last
       
    86     result.toList
       
    87   }
    98   }
    88 
    99 
    89 
   100 
    90   /* information associated with text range */
   101   /* information associated with text range */
    91 
   102