# HG changeset patch
# User immler@in.tum.de
# Date 1251363069 -7200
# Node ID bcae80cc4170ef099bfee5dc1189a1f770cf0938
# Parent  74cc10b5ba5133e7f983c1ba8d6e3bbd4141ed9e
must unapply edits in reverse order

diff -r 74cc10b5ba51 -r bcae80cc4170 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)
     }