src/Pure/Thy/text_edit.scala
author wenzelm
Wed Jan 06 23:18:44 2010 +0100 (2010-01-06)
changeset 34286 951aa92d06bb
parent 34276 12436485c244
child 34302 9bb71dfe7314
permissions -rw-r--r--
more text edit operations;
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@34286
    14
  def after(offset: Int): Int
wenzelm@34276
    15
  def before(offset: Int): Int
wenzelm@34286
    16
  def edit(string: String, shift: Int): (Option[Text_Edit], String)
wenzelm@34276
    17
}
wenzelm@34276
    18
wenzelm@34276
    19
wenzelm@34276
    20
object Text_Edit
wenzelm@34276
    21
{
wenzelm@34286
    22
  /* transform offsets */
wenzelm@34286
    23
wenzelm@34286
    24
  private def after_insert(start: Int, text: String, offset: Int): Int =
wenzelm@34286
    25
    if (start <= offset) offset + text.length
wenzelm@34286
    26
    else offset
wenzelm@34286
    27
wenzelm@34286
    28
  private def after_remove(start: Int, text: String, offset: Int): Int =
wenzelm@34286
    29
    if (start > offset) offset
wenzelm@34286
    30
    else (offset - text.length) max start
wenzelm@34286
    31
wenzelm@34286
    32
wenzelm@34286
    33
  /* edit strings */
wenzelm@34286
    34
wenzelm@34286
    35
  private def insert(index: Int, text: String, string: String): String =
wenzelm@34286
    36
    string.substring(0, index) + text + string.substring(index)
wenzelm@34286
    37
wenzelm@34286
    38
  private def remove(index: Int, count: Int, string: String): String =
wenzelm@34286
    39
    string.substring(0, index) + string.substring(index + count)
wenzelm@34286
    40
wenzelm@34286
    41
wenzelm@34286
    42
  /* explicit edits */
wenzelm@34286
    43
wenzelm@34276
    44
  case class Insert(start: Int, text: String) extends Text_Edit
wenzelm@34276
    45
  {
wenzelm@34286
    46
    def after(offset: Int): Int = after_insert(start, text, offset)
wenzelm@34286
    47
    def before(offset: Int): Int = after_remove(start, text, offset)
wenzelm@34276
    48
wenzelm@34286
    49
    def can_edit(string_length: Int, shift: Int): Boolean =
wenzelm@34286
    50
      shift <= start && start <= shift + string_length
wenzelm@34286
    51
wenzelm@34286
    52
    def edit(string: String, shift: Int): (Option[Insert], String) =
wenzelm@34286
    53
      if (can_edit(string.length, shift)) (None, insert(start - shift, text, string))
wenzelm@34286
    54
      else (Some(this), string)
wenzelm@34276
    55
  }
wenzelm@34276
    56
wenzelm@34276
    57
  case class Remove(start: Int, text: String) extends Text_Edit
wenzelm@34276
    58
  {
wenzelm@34286
    59
    def after(offset: Int): Int = after_remove(start, text, offset)
wenzelm@34286
    60
    def before(offset: Int): Int = after_insert(start, text, offset)
wenzelm@34286
    61
wenzelm@34286
    62
    def can_edit(string_length: Int, shift: Int): Boolean =
wenzelm@34286
    63
      shift <= start && start < shift + string_length
wenzelm@34276
    64
wenzelm@34286
    65
    def edit(string: String, shift: Int): (Option[Remove], String) =
wenzelm@34286
    66
      if (can_edit(string.length, shift)) {
wenzelm@34286
    67
        val index = start - shift
wenzelm@34286
    68
        val count = text.length min (string.length - index)
wenzelm@34286
    69
        val rest =
wenzelm@34286
    70
          if (count == text.length) None
wenzelm@34286
    71
          else Some(Remove(start, text.substring(count)))
wenzelm@34286
    72
        (rest, remove(index, count, string))
wenzelm@34286
    73
      }
wenzelm@34286
    74
      else (Some(this), string)
wenzelm@34276
    75
  }
wenzelm@34276
    76
}
wenzelm@34276
    77