--- 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