author | wenzelm |
Tue, 09 Dec 2014 19:39:40 +0100 | |
changeset 59119 | c90c02940964 |
parent 56860 | dc71c3d0e909 |
child 59136 | c2b23cb8a677 |
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 |
{ |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
19 |
/* plain thread */ |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
20 |
|
39577 | 21 |
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
22 |
{ |
39577 | 23 |
val thread = |
24 |
if (name == null || name == "") new Thread() { override def run = body } |
|
25 |
else new Thread(name) { override def run = body } |
|
38638 | 26 |
thread.setDaemon(daemon) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
27 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
28 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
29 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
30 |
|
39579 | 31 |
|
32 |
/* future result via thread */ |
|
39577 | 33 |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
34 |
def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) = |
39577 | 35 |
{ |
36 |
val result = Future.promise[A] |
|
48355
6b36da29a0bf
support for detached Bash_Job with some control operations;
wenzelm
parents:
45673
diff
changeset
|
37 |
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
|
38 |
(thread, result) |
39577 | 39 |
} |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
40 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
41 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
42 |
/* thread pool */ |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
43 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
44 |
lazy val default_pool = ForkJoinTasks.defaultForkJoinPool |
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
45 |
|
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
46 |
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
|
47 |
default_pool.submit(new Callable[A] { def call = body }) |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
48 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
49 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
50 |
/* delayed events */ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
51 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
52 |
final class Delay private [Simple_Thread](first: Boolean, delay: => Time, event: => Unit) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
53 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
54 |
private var running: Option[Event_Timer.Request] = None |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
55 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
56 |
private def run: Unit = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
57 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
58 |
val do_run = synchronized { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
59 |
if (running.isDefined) { running = None; true } else false |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
60 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
61 |
if (do_run) event |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
62 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
63 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
64 |
def invoke(): Unit = synchronized |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
65 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
66 |
val new_run = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
67 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
68 |
case Some(request) => if (first) false else { request.cancel; true } |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
69 |
case None => true |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
70 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
71 |
if (new_run) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
72 |
running = Some(Event_Timer.request(Time.now() + delay)(run)) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
73 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
74 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
75 |
def revoke(): Unit = synchronized |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
76 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
77 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
78 |
case Some(request) => request.cancel; running = None |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
79 |
case None => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
80 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
81 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
82 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
83 |
def postpone(alt_delay: Time): Unit = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
84 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
85 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
86 |
case Some(request) => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
87 |
val alt_time = Time.now() + alt_delay |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
88 |
if (request.time < alt_time && request.cancel) { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
89 |
running = Some(Event_Timer.request(alt_time)(run)) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
90 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
91 |
case None => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
92 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
93 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
94 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
95 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
96 |
// delayed event after first invocation |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
97 |
def delay_first(delay: => Time)(event: => Unit): Delay = new Delay(true, delay, event) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
98 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
99 |
// delayed event after last invocation |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
100 |
def delay_last(delay: => Time)(event: => Unit): Delay = new Delay(false, delay, event) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
101 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
102 |