# HG changeset patch
# User wenzelm
# Date 1281434993 -7200
# Node ID dd7dcb9b2637122ae0380ea870c41e314947afd7
# Parent  f0fd14a9c11f007b2040069cf23957ace58e55b4
added Library.thread_actor -- thread as actor;

diff -r f0fd14a9c11f -r dd7dcb9b2637 src/Pure/library.scala
--- a/src/Pure/library.scala	Tue Aug 10 12:08:24 2010 +0200
+++ b/src/Pure/library.scala	Tue Aug 10 12:09:53 2010 +0200
@@ -6,11 +6,12 @@
 
 package isabelle
 
-import java.lang.System
+
+import java.lang.{System, Thread}
 import java.awt.Component
 import javax.swing.JOptionPane
 
-
+import scala.actors.Actor
 import scala.swing.ComboBox
 import scala.swing.event.SelectionChanged
 
@@ -138,4 +139,15 @@
         ((stop - start).toDouble / 1000000) + "ms elapsed time")
     Exn.release(result)
   }
+
+
+  /* thread as actor */
+
+  def thread_actor(name: String)(body: => Unit): Actor =
+  {
+    val actor = Future.promise[Actor]
+    val thread = new Thread(name) { override def run() = { actor.fulfill(Actor.self); body } }
+    thread.start
+    actor.join
+  }
 }