src/Pure/Thy/text_edit.scala
changeset 34276 12436485c244
child 34286 951aa92d06bb
equal deleted inserted replaced
34275:8f105e6a2b88 34276:12436485c244
       
     1 /*  Title:      Pure/Thy/text_edit.scala
       
     2     Author:     Fabian Immler, TU Munich
       
     3     Author:     Makarius
       
     4 
       
     5 Basic edits on plain text.
       
     6 */
       
     7 
       
     8 package isabelle
       
     9 
       
    10 
       
    11 sealed abstract class Text_Edit
       
    12 {
       
    13   val start: Int
       
    14   def before(offset: Int): Int
       
    15   def after(offset: Int): Int
       
    16 }
       
    17 
       
    18 
       
    19 object Text_Edit
       
    20 {
       
    21   case class Insert(start: Int, text: String) extends Text_Edit
       
    22   {
       
    23     def before(offset: Int): Int =
       
    24       if (start > offset) offset
       
    25       else (offset - text.length) max start
       
    26 
       
    27     def after(offset: Int): Int =
       
    28       if (start <= offset) offset + text.length
       
    29       else offset
       
    30   }
       
    31 
       
    32   case class Remove(start: Int, text: String) extends Text_Edit
       
    33   {
       
    34     def before(offset: Int): Int =
       
    35       if (start <= offset) offset + text.length
       
    36       else offset
       
    37 
       
    38     def after(offset: Int): Int =
       
    39       if (start > offset) offset
       
    40       else (offset - text.length) max start
       
    41   }
       
    42 }
       
    43