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

 package isabelle.jedit
 
 
 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
 
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}

 {
   /* changes vs. edits */
 
   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
 
   private val edits = new mutable.ListBuffer[Edit]   // owned by Swing thread

   private val edits_delay = Swing_Thread.delay_last(300) {
     if (!edits.isEmpty) {
       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)
       current_change = change2
       edits.clear

   /* history of changes */
 
   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)
   }