# HG changeset patch
# User immler@in.tum.de
# Date 1252324356 -7200
# Node ID 39e3039645ae6c5f55c43b0b1adf199673a82325
# Parent  3f32e08bbb6cc4b05926f0204c35e0ed5ea58c4d
corrected order

diff -r 3f32e08bbb6c -r 39e3039645ae src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Sep 06 22:27:32 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Sep 07 13:52:36 2009 +0200
@@ -197,14 +197,15 @@
 
   /* transforming offsets */
 
-  private def changes_to(doc: ProofDocument): List[Edit] =
-    edits.toList ::: List.flatten(current_change.ancestors(_.id == doc.id).map(_.edits))
+  private def changes_from(doc: ProofDocument): List[Edit] =
+    List.flatten(current_change.ancestors(_.id == doc.id).reverse.map(_.edits)) :::
+      edits.toList
 
   def from_current(doc: ProofDocument, offset: Int): Int =
-    (offset /: changes_to(doc)) ((i, change) => change before i)
+    (offset /: changes_from(doc).reverse) ((i, change) => change before i)
 
   def to_current(doc: ProofDocument, offset: Int): Int =
-    (offset /: changes_to(doc).reverse) ((i, change) => change after i)
+    (offset /: changes_from(doc)) ((i, change) => change after i)
 
 
   private def lines_of_command(cmd: Command) =