src/Pure/PIDE/text.scala
changeset 38425 e467db701d78
parent 38154 343cb5d4034a
child 38426 2858ec7b6dd8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/text.scala	Sun Aug 15 21:42:13 2010 +0200
     1.3 @@ -0,0 +1,61 @@
     1.4 +/*  Title:      Pure/PIDE/text.scala
     1.5 +    Author:     Fabian Immler, TU Munich
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Basic operations on plain text.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +object Text
    1.15 +{
    1.16 +  /* edits */
    1.17 +
    1.18 +  object Edit
    1.19 +  {
    1.20 +    def insert(start: Int, text: String): Edit = new Edit(true, start, text)
    1.21 +    def remove(start: Int, text: String): Edit = new Edit(false, start, text)
    1.22 +  }
    1.23 +
    1.24 +  class Edit(val is_insert: Boolean, val start: Int, val text: String)
    1.25 +  {
    1.26 +    override def toString =
    1.27 +      (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    1.28 +
    1.29 +
    1.30 +    /* transform offsets */
    1.31 +
    1.32 +    private def transform(do_insert: Boolean, offset: Int): Int =
    1.33 +      if (offset < start) offset
    1.34 +      else if (is_insert == do_insert) offset + text.length
    1.35 +      else (offset - text.length) max start
    1.36 +
    1.37 +    def convert(offset: Int): Int = transform(true, offset)
    1.38 +    def revert(offset: Int): Int = transform(false, offset)
    1.39 +
    1.40 +
    1.41 +    /* edit strings */
    1.42 +
    1.43 +    private def insert(index: Int, string: String): String =
    1.44 +      string.substring(0, index) + text + string.substring(index)
    1.45 +
    1.46 +    private def remove(index: Int, count: Int, string: String): String =
    1.47 +      string.substring(0, index) + string.substring(index + count)
    1.48 +
    1.49 +    def can_edit(string: String, shift: Int): Boolean =
    1.50 +      shift <= start && start < shift + string.length
    1.51 +
    1.52 +    def edit(string: String, shift: Int): (Option[Edit], String) =
    1.53 +      if (!can_edit(string, shift)) (Some(this), string)
    1.54 +      else if (is_insert) (None, insert(start - shift, string))
    1.55 +      else {
    1.56 +        val index = start - shift
    1.57 +        val count = text.length min (string.length - index)
    1.58 +        val rest =
    1.59 +          if (count == text.length) None
    1.60 +          else Some(Edit.remove(start, text.substring(count)))
    1.61 +        (rest, remove(index, count, string))
    1.62 +      }
    1.63 +  }
    1.64 +}