| author | wenzelm | 
| Sun, 26 Feb 2012 18:25:28 +0100 | |
| changeset 46684 | 7f741b2c82a3 | 
| parent 45673 | cd41e3903fbf | 
| child 48355 | 6b36da29a0bf | 
| permissions | -rw-r--r-- | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 1 | /* Title: Pure/Concurrent/simple_thread.scala | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45667diff
changeset | 2 | Module: PIDE | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 3 | Author: Makarius | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 4 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 5 | Simplified thread operations. | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 6 | */ | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 7 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 8 | package isabelle | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 9 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 10 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 11 | import java.lang.Thread | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 12 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 13 | import scala.actors.Actor | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 14 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 15 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 16 | object Simple_Thread | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 17 | {
 | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 18 | /* plain thread */ | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 19 | |
| 39577 | 20 | def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 21 |   {
 | 
| 39577 | 22 | val thread = | 
| 23 |       if (name == null || name == "") new Thread() { override def run = body }
 | |
| 24 |       else new Thread(name) { override def run = body }
 | |
| 38638 | 25 | thread.setDaemon(daemon) | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 26 | thread.start | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 27 | thread | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 28 | } | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 29 | |
| 39579 | 30 | |
| 31 | /* future result via thread */ | |
| 39577 | 32 | |
| 33 | def future[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] = | |
| 34 |   {
 | |
| 35 | val result = Future.promise[A] | |
| 36 |     fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
 | |
| 37 | result | |
| 38 | } | |
| 39 | ||
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 40 | |
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 41 | /* thread as actor */ | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 42 | |
| 39572 | 43 | def actor(name: String, daemon: Boolean = false)(body: => Unit): (Thread, Actor) = | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 44 |   {
 | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 45 | val actor = Future.promise[Actor] | 
| 38638 | 46 |     val thread = fork(name, daemon) { actor.fulfill(Actor.self); body }
 | 
| 39572 | 47 | (thread, actor.join) | 
| 38636 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 48 | } | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 49 | } | 
| 
b7647ca7de5a
module for simplified thread operations (Scala version);
 wenzelm parents: diff
changeset | 50 |