minor tuning;

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Sep 02 22:21:14 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Sep 03 11:52:05 2009 +0200
@@ -170,12 +170,6 @@
 
   /* BufferListener methods */
 
-  override def contentInserted(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
-  override def contentRemoved(buffer: JEditBuffer,
-    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
-
   override def preContentInserted(buffer: JEditBuffer,
     start_line: Int, offset: Int, num_lines: Int, length: Int)
   {
@@ -190,6 +184,12 @@
     edits_delay()
   }
 
+  override def contentInserted(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
+  override def contentRemoved(buffer: JEditBuffer,
+    start_line: Int, offset: Int, num_lines: Int, length: Int) { }
+
   override def bufferLoaded(buffer: JEditBuffer) { }
   override def foldHandlerChanged(buffer: JEditBuffer) { }
   override def foldLevelChanged(buffer: JEditBuffer, start_line: Int, end_line: Int) { }
@@ -201,11 +201,11 @@
   private def changes_to(doc: ProofDocument): List[Edit] =
     edits.toList ::: List.flatten(current_change.ancestors(_.id == doc.id).map(_.edits))
 
-  def from_current(doc: ProofDocument, pos: Int) =
-    (pos /: changes_to(doc)) ((p, c) => c from_where p)
+  def from_current(doc: ProofDocument, offset: Int): Int =
+    (offset /: changes_to(doc)) ((i, change) => change before i)
 
-  def to_current(doc: ProofDocument, pos: Int) =
-    (pos /: changes_to(doc).reverse) ((p, c) => c where_to p)
+  def to_current(doc: ProofDocument, offset: Int): Int =
+    (offset /: changes_to(doc).reverse) ((i, change) => change after i)
 
 
   private def lines_of_command(cmd: Command) =

--- a/src/Tools/jEdit/src/proofdocument/Change.scala	Wed Sep 02 22:21:14 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Change.scala	Thu Sep 03 11:52:05 2009 +0200
@@ -10,28 +10,28 @@
 sealed abstract class Edit
 {
   val start: Int
-  def from_where (x: Int): Int //where has x been before applying this edit
-  def where_to(x: Int): Int //where will x be when we apply this edit
+  def before(offset: Int): Int
+  def after(offset: Int): Int
 }
 
 case class Insert(start: Int, text: String) extends Edit
 {
-  def from_where(x: Int) =
-    if (start > x) x
-    else (x - text.length) max start
+  def before(offset: Int): Int =
+    if (start > offset) offset
+    else (offset - text.length) max start
 
-  def where_to(x: Int) =
-    if (start <= x) x + text.length else x
+  def after(offset: Int): Int =
+    if (start <= offset) offset + text.length else offset
 }
 
 case class Remove(start: Int, text: String) extends Edit
 {
-  def from_where(x: Int) =
-    if (start <= x) x + text.length else x
+  def before(offset: Int): Int =
+    if (start <= offset) offset + text.length else offset
 
-  def where_to(x: Int) =
-    if (start > x) x
-    else (x - text.length) max start
+  def after(offset: Int): Int =
+    if (start > offset) offset
+    else (offset - text.length) max start
 }
 // TODO: merge multiple inserts?