--- a/src/Pure/Concurrent/standard_thread.scala Tue Nov 03 16:35:00 2015 +0100
+++ b/src/Pure/Concurrent/standard_thread.scala Tue Nov 03 16:35:38 2015 +0100
@@ -28,19 +28,9 @@
}
- /* future result via thread */
-
- def future[A](name: String = "", daemon: Boolean = false)(body: => A): (Thread, Future[A]) =
- {
- val result = Future.promise[A]
- val thread = fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
- (thread, result)
- }
-
-
/* thread pool */
- lazy val default_pool =
+ lazy val pool: ThreadPoolExecutor =
{
val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
@@ -48,7 +38,7 @@
}
def submit_task[A](body: => A): JFuture[A] =
- default_pool.submit(new Callable[A] { def call = body })
+ pool.submit(new Callable[A] { def call = body })
/* delayed events */