must unapply edits in reverse order
authorimmler@in.tum.de
Thu, 27 Aug 2009 10:51:09 +0200
changeset 34682 bcae80cc4170
parent 34681 74cc10b5ba51
child 34683 fe7bedf0cfc9
must unapply edits in reverse order
src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 10:51:09 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Thu Aug 27 10:51:09 2009 +0200
@@ -113,7 +113,7 @@
       case Remove(start, removed) => buffer.remove(start, removed.length)
     }
 
-    def unapply(c: Change) = c.map {
+    def unapply(c: Change) = c.toList.reverse.map {
       case Insert(start, added) => buffer.remove(start, added.length)
       case Remove(start, removed) => buffer.insert(start, removed)
     }