| author | wenzelm | 
| Wed, 01 Aug 2012 15:50:50 +0200 | |
| changeset 48635 | bfce940c6f38 | 
| parent 48355 | 6b36da29a0bf | 
| child 49471 | 97964515a676 | 
| 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: 
45667 
diff
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  | 
|
| 
48355
 
6b36da29a0bf
support for detached Bash_Job with some control operations;
 
wenzelm 
parents: 
45673 
diff
changeset
 | 
33  | 
def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =  | 
| 39577 | 34  | 
  {
 | 
35  | 
val result = Future.promise[A]  | 
|
| 
48355
 
6b36da29a0bf
support for detached Bash_Job with some control operations;
 
wenzelm 
parents: 
45673 
diff
changeset
 | 
36  | 
    val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
 | 
| 
 
6b36da29a0bf
support for detached Bash_Job with some control operations;
 
wenzelm 
parents: 
45673 
diff
changeset
 | 
37  | 
(thread, result)  | 
| 39577 | 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  |