src/Pure/PIDE/text.scala
changeset 46712 8650d9a95736
parent 46576 ae9286f64574
child 47542 26d0a76fef0a
     1.1 --- a/src/Pure/PIDE/text.scala	Mon Feb 27 16:56:25 2012 +0100
     1.2 +++ b/src/Pure/PIDE/text.scala	Mon Feb 27 17:13:25 2012 +0100
     1.3 @@ -98,7 +98,8 @@
     1.4      }
     1.5    }
     1.6  
     1.7 -  class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
     1.8 +  final class Perspective private(
     1.9 +    val ranges: List[Range]) // visible text partitioning in canonical order
    1.10    {
    1.11      def is_empty: Boolean = ranges.isEmpty
    1.12      def range: Range =
    1.13 @@ -134,7 +135,7 @@
    1.14      def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
    1.15    }
    1.16  
    1.17 -  class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
    1.18 +  final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
    1.19    {
    1.20      override def toString =
    1.21        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"