# HG changeset patch
# User wenzelm
# Date 1253052841 -7200
# Node ID 34b0aadab7ee7dc50508c9e7e94fb0178e8a6899
# Parent  80408ffc84a8e5778ab9717a1162e3447bb1f665
Linear_Set.append_after;

diff -r 80408ffc84a8 -r 34b0aadab7ee src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Tue Sep 15 21:14:09 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Sep 16 00:14:01 2009 +0200
@@ -230,8 +230,10 @@
     val inserted_commands = tokens_to_commands(rescanning_tokens.toList)
 
     // build new document
-    val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change).
-        insert_after(cmd_before_change, inserted_commands)
+    val new_commandset = commands.
+      delete_between(cmd_before_change, cmd_after_change).
+      append_after(cmd_before_change, inserted_commands)
+
 
     val doc =
       new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset,