1.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 22:11:32 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 22:20:54 2010 +0100
     1.3 @@ -62,18 +62,15 @@
     1.4    private val change_0 = new Change(None, Nil, Future.value(document_0, Nil))
     1.5  
     1.6    @volatile private var history = List(change_0)   // owned by Swing thread
     1.7 -  def changes = history
     1.8 -  def current_change: Change = history.first
     1.9  
    1.10 -
    1.11 -    /* history of changes */
    1.12 +  def current_change(): Change = history.first
    1.13  
    1.14    def recent_document(): Document =
    1.15    {
    1.16      def find(change: Change): Document =
    1.17        if (change.result.is_finished || !change.parent.isDefined) change.document
    1.18        else find(change.parent.get)
    1.19 -    find(current_change)
    1.20 +    find(current_change())
    1.21    }
    1.22  
    1.23  
    1.24 @@ -107,11 +104,11 @@
    1.25    private val edits_delay = Swing_Thread.delay_last(300) {
    1.26      if (!edits_buffer.isEmpty) {
    1.27        val edits = edits_buffer.toList
    1.28 -      val change1 = current_change
    1.29 +      val change1 = current_change()
    1.30        val result: Future[Document.Result] = Future.fork {
    1.31          Document.text_edits(session, change1.document, session.create_id(), edits)
    1.32        }
    1.33 -      val change2 = new Change(Some(change1), edits, result)  // FIXME edits!?
    1.34 +      val change2 = new Change(Some(change1), edits, result)
    1.35        history ::= change2
    1.36        result.map(_ => session.input(change2))
    1.37        edits_buffer.clear