# HG changeset patch
# User immler@in.tum.de
# Date 1239727451 -7200
# Node ID 68a5e91ac3a36150bcd8972717fd33842bcd9fd1
# Parent  3ed38cf4164a2a1ed77816f794ae453c6bc02bf8
fixed shifting;
synchronized commit

diff -r 3ed38cf4164a -r 68a5e91ac3a3 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Apr 07 21:30:47 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Apr 14 18:44:11 2009 +0200
@@ -126,7 +126,7 @@
             if (pos < start + added.length) start
             else pos - added.length + removed
           else pos
-        if (id == to_id) shifted
+        if (id == to_id) pos
         else _from_current(to_id, rest_changes, shifted)
       }
     }
@@ -135,11 +135,12 @@
     changes match {
       case Nil => pos
       case Text.Change(id, start, added, removed) :: rest_changes => {
-        val shifted = if (id == from_id) pos else _to_current(from_id, rest_changes, pos)
-        if (start <= shifted)
+        val shifted = _to_current(from_id, rest_changes, pos)
+        if (id == from_id) pos
+        else if (start <= shifted) {
           if (shifted < start + removed) start
           else shifted + added.length - removed
-        else shifted
+        } else shifted
       }
     }
 
@@ -226,7 +227,7 @@
 
   private var changes: List[Text.Change] = Nil
 
-  private def commit {
+  private def commit: Unit = synchronized {
     if (col != null) {
       changes = col :: changes
       document_actor ! col