ignore unchanged tokens
authorimmler@in.tum.de
Tue, 02 Jun 2009 19:00:58 +0200
changeset 34592 b17ebec3690c
parent 34591 35712cfcfd7a
child 34593 cf37a9f988bf
ignore unchanged tokens
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 _ =>