Future values -- Scala version.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/future.scala	Fri Jan 01 21:26:02 2010 +0100
@@ -0,0 +1,67 @@
+/*  Title:      Pure/Concurrent/future.scala
+    Author:     Makarius
+
+Future values.
+
+Notable differences to scala.actors.Future (as of Scala 2.7.7):
+
+  * We capture/release exceptions as in the ML variant.
+
+  * Future.join works for *any* actor, not just the one of the
+    original fork.
+*/
+
+package isabelle
+
+
+import scala.actors.Actor._
+
+
+object Future
+{
+  def value[A](x: A): Future[A] = new Finished_Future(x)
+  def fork[A](body: => A): Future[A] = new Pending_Future(body)
+}
+
+abstract class Future[A]
+{
+  def peek: Option[Exn.Result[A]]
+  def is_finished: Boolean = peek.isDefined
+  def join: A
+  def map[B](f: A => B): Future[B] = Future.fork { f(join) }
+
+  override def toString =
+    peek match {
+      case None => "<future>"
+      case Some(Exn.Exn(_)) => "<failed>"
+      case Some(Exn.Res(x)) => x.toString
+    }
+}
+
+private class Finished_Future[A](x: A) extends Future[A]
+{
+  val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
+  val join: A = x
+}
+
+private class Pending_Future[A](body: => A) extends Future[A]
+{
+  @volatile private var result: Option[Exn.Result[A]] = None
+
+  private val evaluator = actor {
+    result = Some(Exn.capture(body))
+    loop { react { case _ => reply(result.get) } }
+  }
+
+  def peek: Option[Exn.Result[A]] = result
+
+  def join: A =
+    Exn.release {
+      peek match {
+        case Some(res) => res
+        case None => (evaluator !? ()).asInstanceOf[Exn.Result[A]]
+      }
+    }
+}
+
+

--- a/src/Pure/General/swing_thread.scala	Thu Dec 31 23:47:09 2009 +0100
+++ b/src/Pure/General/swing_thread.scala	Fri Jan 01 21:26:02 2010 +0100
@@ -10,8 +10,6 @@
 import javax.swing.{SwingUtilities, Timer}
 import java.awt.event.{ActionListener, ActionEvent}
 
-import scala.actors.{Future, Futures}
-
 
 object Swing_Thread
 {
@@ -31,8 +29,7 @@
     result.get
   }
 
-  def future[A](body: => A): Future[A] =
-    Futures.future(now(body))
+  def future[A](body: => A): Future[A] = Future.fork { now(body) }
 
   def later(body: => Unit) {
     if (SwingUtilities.isEventDispatchThread()) body

--- a/src/Pure/IsaMakefile	Thu Dec 31 23:47:09 2009 +0100
+++ b/src/Pure/IsaMakefile	Fri Jan 01 21:26:02 2010 +0100
@@ -121,12 +121,13 @@
 
 ## Scala material
 
-SCALA_FILES = General/event_bus.scala General/exn.scala			\
-  General/linear_set.scala General/markup.scala General/position.scala	\
-  General/scan.scala General/swing_thread.scala General/symbol.scala	\
-  General/xml.scala General/yxml.scala Isar/isar_document.scala		\
-  Isar/outer_keyword.scala Isar/outer_lex.scala Isar/outer_parse.scala	\
-  Isar/outer_syntax.scala System/cygwin.scala System/gui_setup.scala	\
+SCALA_FILES = Concurrent/future.scala General/event_bus.scala		\
+  General/exn.scala General/linear_set.scala General/markup.scala	\
+  General/position.scala General/scan.scala General/swing_thread.scala	\
+  General/symbol.scala General/xml.scala General/yxml.scala		\
+  Isar/isar_document.scala Isar/outer_keyword.scala			\
+  Isar/outer_lex.scala Isar/outer_parse.scala Isar/outer_syntax.scala	\
+  System/cygwin.scala System/gui_setup.scala				\
   System/isabelle_process.scala System/isabelle_syntax.scala		\
   System/isabelle_system.scala System/platform.scala			\
   System/session_manager.scala System/standard_system.scala		\