1.1 --- a/src/Pure/Thy/text_edit.scala	Wed Jan 06 23:18:12 2010 +0100
     1.2 +++ b/src/Pure/Thy/text_edit.scala	Wed Jan 06 23:18:44 2010 +0100
     1.3 @@ -11,33 +11,67 @@
     1.4  sealed abstract class Text_Edit
     1.5  {
     1.6    val start: Int
     1.7 +  def after(offset: Int): Int
     1.8    def before(offset: Int): Int
     1.9 -  def after(offset: Int): Int
    1.10 +  def edit(string: String, shift: Int): (Option[Text_Edit], String)
    1.11  }
    1.12  
    1.13  
    1.14  object Text_Edit
    1.15  {
    1.16 +  /* transform offsets */
    1.17 +
    1.18 +  private def after_insert(start: Int, text: String, offset: Int): Int =
    1.19 +    if (start <= offset) offset + text.length
    1.20 +    else offset
    1.21 +
    1.22 +  private def after_remove(start: Int, text: String, offset: Int): Int =
    1.23 +    if (start > offset) offset
    1.24 +    else (offset - text.length) max start
    1.25 +
    1.26 +
    1.27 +  /* edit strings */
    1.28 +
    1.29 +  private def insert(index: Int, text: String, string: String): String =
    1.30 +    string.substring(0, index) + text + string.substring(index)
    1.31 +
    1.32 +  private def remove(index: Int, count: Int, string: String): String =
    1.33 +    string.substring(0, index) + string.substring(index + count)
    1.34 +
    1.35 +
    1.36 +  /* explicit edits */
    1.37 +
    1.38    case class Insert(start: Int, text: String) extends Text_Edit
    1.39    {
    1.40 -    def before(offset: Int): Int =
    1.41 -      if (start > offset) offset
    1.42 -      else (offset - text.length) max start
    1.43 +    def after(offset: Int): Int = after_insert(start, text, offset)
    1.44 +    def before(offset: Int): Int = after_remove(start, text, offset)
    1.45  
    1.46 -    def after(offset: Int): Int =
    1.47 -      if (start <= offset) offset + text.length
    1.48 -      else offset
    1.49 +    def can_edit(string_length: Int, shift: Int): Boolean =
    1.50 +      shift <= start && start <= shift + string_length
    1.51 +
    1.52 +    def edit(string: String, shift: Int): (Option[Insert], String) =
    1.53 +      if (can_edit(string.length, shift)) (None, insert(start - shift, text, string))
    1.54 +      else (Some(this), string)
    1.55    }
    1.56  
    1.57    case class Remove(start: Int, text: String) extends Text_Edit
    1.58    {
    1.59 -    def before(offset: Int): Int =
    1.60 -      if (start <= offset) offset + text.length
    1.61 -      else offset
    1.62 +    def after(offset: Int): Int = after_remove(start, text, offset)
    1.63 +    def before(offset: Int): Int = after_insert(start, text, offset)
    1.64  
    1.65 -    def after(offset: Int): Int =
    1.66 -      if (start > offset) offset
    1.67 -      else (offset - text.length) max start
    1.68 +    def can_edit(string_length: Int, shift: Int): Boolean =
    1.69 +      shift <= start && start < shift + string_length
    1.70 +
    1.71 +    def edit(string: String, shift: Int): (Option[Remove], String) =
    1.72 +      if (can_edit(string.length, shift)) {
    1.73 +        val index = start - shift
    1.74 +        val count = text.length min (string.length - index)
    1.75 +        val rest =
    1.76 +          if (count == text.length) None
    1.77 +          else Some(Remove(start, text.substring(count)))
    1.78 +        (rest, remove(index, count, string))
    1.79 +      }
    1.80 +      else (Some(this), string)
    1.81    }
    1.82  }
    1.83