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