src/Pure/PIDE/text.scala

 
 import scala.collection.mutable
 import scala.util.Sorting
 
 
-object Text
-{
+object Text {
   /* offset */
 
   type Offset = Int
 
 
   /* range -- with total quasi-ordering */
 
-  object Range
-  {
+  object Range {
     def apply(start: Offset): Range = Range(start, start)
 
     val full: Range = apply(0, Integer.MAX_VALUE / 2)
     val offside: Range = apply(-1)
 
-    object Ordering extends scala.math.Ordering[Range]
-    {
+    object Ordering extends scala.math.Ordering[Range] {
       def compare(r1: Range, r2: Range): Int = r1 compare r2
     }
   }
 
-  sealed case class Range(start: Offset, stop: Offset)
-  {
+  sealed case class Range(start: Offset, stop: Offset) {
     // denotation: {start} Un {i. start < i & i < stop}
     if (start > stop)
       error("Bad range: [" + start.toString + ".." + stop.toString + "]")
 
     override def toString: String = "[" + start.toString + ".." + stop.toString + "]"

   }
 
 
   /* perspective */
 
-  object Perspective
-  {
+  object Perspective {
     val empty: Perspective = Perspective(Nil)
 
     def full: Perspective = Perspective(List(Range.full))
 
-    def apply(ranges: List[Range]): Perspective =
-    {
+    def apply(ranges: List[Range]): Perspective = {
       val result = new mutable.ListBuffer[Range]
       var last: Option[Range] = None
       def ship(next: Option[Range]): Unit = { result ++= last; last = next }
 
-      for (range <- ranges.sortBy(_.start))
-      {
+      for (range <- ranges.sortBy(_.start)) {
         last match {
           case None => ship(Some(range))
           case Some(last_range) =>
             last_range.try_join(range) match {
               case None => ship(Some(range))

       new Perspective(result.toList)
     }
   }
 
   final class Perspective private(
-    val ranges: List[Range]) // visible text partitioning in canonical order
-  {
+    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)
 

   }
 
 
   /* information associated with text range */
 
-  sealed case class Info[A](range: Range, info: A)
-  {
+  sealed case class Info[A](range: Range, info: A) {
     def restrict(r: Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
 
     def map[B](f: A => B): Info[B] = Info(range, f(info))
   }

   type Markup = Info[XML.Elem]
 
 
   /* editing */
 
-  object Edit
-  {
+  object Edit {
     def insert(start: Offset, text: String): Edit = new Edit(true, start, text)
     def remove(start: Offset, text: String): Edit = new Edit(false, start, text)
     def inserts(start: Offset, text: String): List[Edit] =
       if (text == "") Nil else List(insert(start, text))
     def removes(start: Offset, text: String): List[Edit] =

     def replace(start: Offset, old_text: String, new_text: String): List[Edit] =
       if (old_text == new_text) Nil
       else removes(start, old_text) ::: inserts(start, new_text)
   }
 
-  final 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: String =
       (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
 
 
     /* transform offsets */