author | wenzelm |
Thu, 24 Apr 2014 22:20:36 +0200 | |
changeset 56707 | aa4631879df8 |
parent 56704 | c2f0ddd14747 |
child 56730 | e723f041b6d0 |
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 |
|
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
14 |
object Simple_Thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
15 |
{ |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
49471
diff
changeset
|
16 |
/* pending interrupts */ |
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
17 |
|
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
18 |
def interrupted_exception(): Unit = |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
49471
diff
changeset
|
19 |
if (Thread.interrupted()) throw Exn.Interrupt() |
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
20 |
|
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
21 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
22 |
/* plain thread */ |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
23 |
|
39577 | 24 |
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
25 |
{ |
39577 | 26 |
val thread = |
27 |
if (name == null || name == "") new Thread() { override def run = body } |
|
28 |
else new Thread(name) { override def run = body } |
|
38638 | 29 |
thread.setDaemon(daemon) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
30 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
31 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
32 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
33 |
|
39579 | 34 |
|
35 |
/* future result via thread */ |
|
39577 | 36 |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
37 |
def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) = |
39577 | 38 |
{ |
39 |
val result = Future.promise[A] |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
40 |
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
|
41 |
(thread, result) |
39577 | 42 |
} |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
43 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
44 |