author | wenzelm |
Fri, 25 Apr 2014 21:31:39 +0200 | |
changeset 56730 | e723f041b6d0 |
parent 56707 | aa4631879df8 |
child 56770 | e160ae47db94 |
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 |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
12 |
import java.util.concurrent.{Callable, Future => JFuture} |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
13 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
14 |
import scala.collection.parallel.ForkJoinTasks |
38636
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 |
|
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
17 |
object Simple_Thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
18 |
{ |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
49471
diff
changeset
|
19 |
/* pending interrupts */ |
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 |
def interrupted_exception(): Unit = |
56667
65e84b0ef974
more abstract Exn.Interrupt and POSIX return code;
wenzelm
parents:
49471
diff
changeset
|
22 |
if (Thread.interrupted()) throw Exn.Interrupt() |
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
23 |
|
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
48355
diff
changeset
|
24 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
25 |
/* plain thread */ |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
26 |
|
39577 | 27 |
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
28 |
{ |
39577 | 29 |
val thread = |
30 |
if (name == null || name == "") new Thread() { override def run = body } |
|
31 |
else new Thread(name) { override def run = body } |
|
38638 | 32 |
thread.setDaemon(daemon) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
33 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
34 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
35 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
36 |
|
39579 | 37 |
|
38 |
/* future result via thread */ |
|
39577 | 39 |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
40 |
def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) = |
39577 | 41 |
{ |
42 |
val result = Future.promise[A] |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
43 |
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
|
44 |
(thread, result) |
39577 | 45 |
} |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
46 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
47 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
48 |
/* thread pool */ |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
49 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
50 |
lazy val default_pool = ForkJoinTasks.defaultForkJoinPool |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
51 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
52 |
def submit_task[A](body: => A): JFuture[A] = |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
53 |
default_pool.submit(new Callable[A] { def call = body }) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
54 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
55 |