equal
deleted
inserted
replaced
10 import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory} |
10 import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory} |
11 |
11 |
12 |
12 |
13 object Isabelle_Thread |
13 object Isabelle_Thread |
14 { |
14 { |
15 /* fork */ |
15 /* self-thread */ |
|
16 |
|
17 def self: Isabelle_Thread = |
|
18 Thread.currentThread match { |
|
19 case thread: Isabelle_Thread => thread |
|
20 case _ => error("Isabelle-specific thread required") |
|
21 } |
|
22 |
|
23 |
|
24 /* fork threads */ |
16 |
25 |
17 private val counter = Counter.make() |
26 private val counter = Counter.make() |
18 |
27 |
19 def make_name(name: String = "", base: String = "thread"): String = |
28 def make_name(name: String = "", base: String = "thread"): String = |
20 "Isabelle." + proper_string(name).getOrElse(base + counter()) |
29 "Isabelle." + proper_string(name).getOrElse(base + counter()) |
38 thread.start |
47 thread.start |
39 thread |
48 thread |
40 } |
49 } |
41 |
50 |
42 |
51 |
43 /* self-thread */ |
52 /* thread pool */ |
44 |
53 |
45 def self: Isabelle_Thread = |
54 lazy val pool: ThreadPoolExecutor = |
46 Thread.currentThread match { |
55 { |
47 case thread: Isabelle_Thread => thread |
56 val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
48 case _ => error("Isabelle-specific thread required") |
57 val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 |
49 } |
58 val executor = |
|
59 new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) |
|
60 executor.setThreadFactory( |
|
61 new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group)) |
|
62 executor |
|
63 } |
50 |
64 |
51 |
65 |
52 /* interrupt handlers */ |
66 /* interrupt handlers */ |
53 |
67 |
54 object Interrupt_Handler |
68 object Interrupt_Handler |
79 def interruptible[A](body: => A): A = |
93 def interruptible[A](body: => A): A = |
80 interrupt_handler(Interrupt_Handler.interruptible)(body) |
94 interrupt_handler(Interrupt_Handler.interruptible)(body) |
81 |
95 |
82 def uninterruptible[A](body: => A): A = |
96 def uninterruptible[A](body: => A): A = |
83 interrupt_handler(Interrupt_Handler.uninterruptible)(body) |
97 interrupt_handler(Interrupt_Handler.uninterruptible)(body) |
84 |
|
85 |
|
86 /* thread pool */ |
|
87 |
|
88 lazy val pool: ThreadPoolExecutor = |
|
89 { |
|
90 val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
|
91 val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 |
|
92 val executor = |
|
93 new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) |
|
94 executor.setThreadFactory( |
|
95 new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group)) |
|
96 executor |
|
97 } |
|
98 |
98 |
99 |
99 |
100 /* delayed events */ |
100 /* delayed events */ |
101 |
101 |
102 final class Delay private[Isabelle_Thread]( |
102 final class Delay private[Isabelle_Thread]( |