diff -r 7407bc6cf28d -r b06946a1d4cb src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Feb 02 23:08:44 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Mar 02 19:27:06 2009 +0100
@@ -219,7 +219,8 @@
       else if (after_change != null)
         after_change.prev = before_change
     }
-    
+
+    System.err.println("token_changed: " + before_change + " " + after_change + " " + first_removed)
     token_changed(before_change, after_change, first_removed)
   }