# HG changeset patch
# User wenzelm
# Date 1262381348 -3600
# Node ID 621753b73219ad50bcc7ea74dd85f324335d82c9
# Parent  e75ff2d8819e71b15eaff3eb12280dd9041e4d8e
tuned;

diff -r e75ff2d8819e -r 621753b73219 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 22:20:54 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 22:29:08 2010 +0100
@@ -58,12 +58,10 @@
 {
   /* history */
 
-  private val document_0 = session.begin_document(buffer.getName)
-  private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
+  @volatile private var history =  // owned by Swing thread
+    new Change(None, Nil, Future.value(session.begin_document(buffer.getName), Nil))
 
-  @volatile private var history = List(change_0)   // owned by Swing thread
-
-  def current_change(): Change = history.first
+  def current_change(): Change = history
 
   def recent_document(): Document =
   {
@@ -109,7 +107,7 @@
         Document.text_edits(session, change1.document, session.create_id(), edits)
       }
       val change2 = new Change(Some(change1), edits, result)
-      history ::= change2
+      history = change2
       result.map(_ => session.input(change2))
       edits_buffer.clear
     }