# HG changeset patch
# User immler@in.tum.de
# Date 1239132647 -7200
# Node ID 3ed38cf4164a2a1ed77816f794ae453c6bc02bf8
# Parent  b928628742edafc578fe845a282f386c7ba6df68
correct order, added curreeeent change

diff -r b928628742ed -r 3ed38cf4164a src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 06 20:01:33 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Tue Apr 07 21:30:47 2009 +0200
@@ -143,8 +143,10 @@
       }
     }
 
-  def to_current(from_id: String, pos : Int) = _to_current(from_id, changes, pos)
-  def from_current(to_id: String, pos : Int) = _from_current(to_id, changes, pos)
+  def to_current(from_id: String, pos : Int) =
+    _to_current(from_id, if (col == null) changes else col :: changes, pos)
+  def from_current(to_id: String, pos : Int) =
+    _from_current(to_id, if (col == null) changes else col :: changes, pos)
 
   def repaint(cmd: Command) =
   {
@@ -226,7 +228,7 @@
 
   private def commit {
     if (col != null) {
-      changes += col
+      changes = col :: changes
       document_actor ! col
     }
     col = null