--- a/src/Pure/PIDE/change.scala Thu Aug 05 18:13:12 2010 +0200
+++ b/src/Pure/PIDE/change.scala Thu Aug 05 18:17:59 2010 +0200
@@ -74,8 +74,8 @@
val document = stable.join_document
val node = document.nodes(name)
val is_outdated = !(extra_edits.isEmpty && latest == stable)
- def convert(offset: Int): Int = (offset /: changes)((i, change) => change after i)
- def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change before i) // FIXME fold_rev (!?)
+ def convert(offset: Int): Int = (offset /: changes)((i, change) => change.convert(i))
+ def revert(offset: Int): Int = (offset /: changes.reverse)((i, change) => change.revert(i)) // FIXME fold_rev (!?)
}
}
}
\ No newline at end of file
--- a/src/Pure/PIDE/text_edit.scala Thu Aug 05 18:13:12 2010 +0200
+++ b/src/Pure/PIDE/text_edit.scala Thu Aug 05 18:17:59 2010 +0200
@@ -21,8 +21,8 @@
else if (is_insert == do_insert) offset + text.length
else (offset - text.length) max start
- def after(offset: Int): Int = transform(true, offset)
- def before(offset: Int): Int = transform(false, offset)
+ def convert(offset: Int): Int = transform(true, offset)
+ def revert(offset: Int): Int = transform(false, offset)
/* edit strings */