# HG changeset patch
# User immler@in.tum.de
# Date 1243962058 -7200
# Node ID b17ebec3690c202e60f29d1d9dc6b395321d3d88
# Parent  35712cfcfd7a66a64aa253a8b52dad7cbbf8e262
ignore unchanged tokens

diff -r 35712cfcfd7a -r b17ebec3690c src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 19:00:58 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Jun 02 19:00:58 2009 +0200
@@ -122,7 +122,8 @@
       invalid_tokens match {
         case t::ts => if(start(t) == start(new_token) &&
                          start(t) > change.start + change.added.length) {
-          old_suffix = ts
+          old_suffix = t::ts
+          new_tokens = new_tokens.tail
           invalid_tokens = Nil
         }
         case _ =>