# HG changeset patch # User wenzelm # Date 1263230662 -3600 # Node ID 265075989f01627b64bad4b350a0d89945e50b06 # Parent f0a6f02ad70594662ae8c56a7aa136de363704b0 simplified Text_Edit -- deflated class hierarchy; diff -r f0a6f02ad705 -r 265075989f01 src/Pure/Thy/text_edit.scala --- a/src/Pure/Thy/text_edit.scala Mon Jan 11 18:23:06 2010 +0100 +++ b/src/Pure/Thy/text_edit.scala Mon Jan 11 18:24:22 2010 +0100 @@ -8,72 +8,40 @@ package isabelle -sealed abstract class Text_Edit -{ - val start: Int - def text: String - def after(offset: Int): Int - def before(offset: Int): Int - def can_edit(string_length: Int, shift: Int): Boolean - def edit(string: String, shift: Int): (Option[Text_Edit], String) -} - - -object Text_Edit +class Text_Edit(val is_insert: Boolean, val start: Int, val text: String) { /* transform offsets */ - private def after_insert(start: Int, text: String, offset: Int): Int = - if (start <= offset) offset + text.length - else offset + private def transform(do_insert: Boolean, offset: Int): Int = + if (offset < start) offset + else if (is_insert == do_insert) offset + text.length + else (offset - text.length) max start - private def after_remove(start: Int, text: String, offset: Int): Int = - if (start > offset) offset - else (offset - text.length) max start + def after(offset: Int): Int = transform(true, offset) + def before(offset: Int): Int = transform(false, offset) /* edit strings */ - private def insert(index: Int, text: String, string: String): String = + private def insert(index: Int, string: String): String = string.substring(0, index) + text + string.substring(index) private def remove(index: Int, count: Int, string: String): String = string.substring(0, index) + string.substring(index + count) - - /* explicit edits */ - - case class Insert(start: Int, text: String) extends Text_Edit - { - def after(offset: Int): Int = after_insert(start, text, offset) - def before(offset: Int): Int = after_remove(start, text, offset) - - def can_edit(string_length: Int, shift: Int): Boolean = - shift <= start && start <= shift + string_length - - def edit(string: String, shift: Int): (Option[Insert], String) = - if (can_edit(string.length, shift)) (None, insert(start - shift, text, string)) - else (Some(this), string) - } + def can_edit(string: String, shift: Int): Boolean = + shift <= start && start < shift + string.length - case class Remove(start: Int, text: String) extends Text_Edit - { - def after(offset: Int): Int = after_remove(start, text, offset) - def before(offset: Int): Int = after_insert(start, text, offset) - - def can_edit(string_length: Int, shift: Int): Boolean = - shift <= start && start < shift + string_length - - def edit(string: String, shift: Int): (Option[Remove], String) = - if (can_edit(string.length, shift)) { - val index = start - shift - val count = text.length min (string.length - index) - val rest = - if (count == text.length) None - else Some(Remove(start, text.substring(count))) - (rest, remove(index, count, string)) - } - else (Some(this), string) - } + def edit(string: String, shift: Int): (Option[Text_Edit], String) = + if (!can_edit(string, shift)) (Some(this), string) + else if (is_insert) (None, insert(start - shift, string)) + else { + val index = start - shift + val count = text.length min (string.length - index) + val rest = + if (count == text.length) None + else Some(new Text_Edit(false, start, text.substring(count))) + (rest, remove(index, count, string)) + } }