# HG changeset patch
# User wenzelm
# Date 1262378257 -3600
# Node ID 7f72547f9b12504d991775056e2e76a3c4e93985
# Parent  ac35eee85f5c7a9770b1b08dd8adf82cc8c36817
use isabelle.Future;
tuned;

diff -r ac35eee85f5c -r 7f72547f9b12 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)
   }
diff -r ac35eee85f5c -r 7f72547f9b12 src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 17:29:35 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Fri Jan 01 21:37:37 2010 +0100
@@ -8,9 +8,6 @@
 package isabelle.proofdocument
 
 
-import scala.actors.Future
-
-
 sealed abstract class Edit
 {
   val start: Int
@@ -54,6 +51,6 @@
     else this :: parent.map(_.ancestors(done)).getOrElse(Nil)
   def ancestors: List[Change] = ancestors(_ => false)
 
-  def document: Document = result()._1
-  def document_edits: List[Document.Structure_Edit] = result()._2
+  def document: Document = result.join._1
+  def document_edits: List[Document.Structure_Edit] = result.join._2
 }
\ No newline at end of file
diff -r ac35eee85f5c -r 7f72547f9b12 src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 17:29:35 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Fri Jan 01 21:37:37 2010 +0100
@@ -9,8 +9,6 @@
 package isabelle.proofdocument
 
 
-import scala.actors.Future
-import scala.actors.Futures._
 import scala.actors.Actor._
 import scala.collection.mutable
 
diff -r ac35eee85f5c -r 7f72547f9b12 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 17:29:35 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Fri Jan 01 21:37:37 2010 +0100
@@ -82,7 +82,7 @@
     {
       require(change.parent.isDefined)
 
-      val (doc, changes) = change.result()  // FIXME clarify future vs. actor arrangement
+      val (doc, changes) = change.result.join
       val id_changes = changes map {
         case (c1, c2) =>
           (c1.map(_.id).getOrElse(""),