src/Tools/jEdit/src/jedit/document_model.scala

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 17:29:35 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Fri Jan 01 21:37:37 2010 +0100
@@ -10,8 +10,6 @@
 
 import isabelle.proofdocument.{Change, Command, Edit, Insert, Remove, Document, Session}
 
-import scala.actors.Future
-import scala.actors.Futures._
 import scala.actors.Actor, Actor._
 import scala.collection.mutable
 
@@ -62,8 +60,7 @@
 
   private val document_0 = session.begin_document(buffer.getName)
 
-  private val change_0 =
-    new Change(document_0.id, None, Nil, future { (document_0, Nil) })  // FIXME more robust history start
+  private val change_0 = new Change(document_0.id, None, Nil, Future.value(document_0, Nil))
   private var _changes = List(change_0)   // owned by Swing thread
   def changes = _changes
   private var current_change = change_0
@@ -75,11 +72,10 @@
       val new_id = session.create_id()
       val eds = edits.toList
       val change1 = current_change
-      val result: Future[Document.Result] = future {
+      val result: Future[Document.Result] = Future.fork {
         val old_doc = change1.document
         Document.text_edits(session, old_doc, new_id, eds)
       }
-      result()  // FIXME !?!?!?
       val change2 = new Change(new_id, Some(change1), eds, result)
       _changes ::= change2
       session.input(change2)
@@ -114,7 +110,7 @@
   def recent_document(): Document =
   {
     def find(change: Change): Document =
-      if (change.result.isSet || !change.parent.isDefined) change.document
+      if (change.result.is_finished || !change.parent.isDefined) change.document
       else find(change.parent.get)
     find(current_change)
   }