src/Pure/PIDE/text.scala

       ship(None)
       new Perspective(result.toList)
     }
   }
 
-  class Perspective private(val ranges: List[Range]) // visible text partitioning in canonical order
+  final class Perspective private(
+    val ranges: List[Range]) // visible text partitioning in canonical order
   {
     def is_empty: Boolean = ranges.isEmpty
     def range: Range =
       if (is_empty) Range(0)
       else Range(ranges.head.start, ranges.last.stop)

   {
     def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
   }
 
-  class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
+  final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
   {
     override def toString =
       (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"