# HG changeset patch # User wenzelm # Date 1446569589 -3600 # Node ID 91c3aedbfc5e2fd230f88237d2678f92e93f9f29 # Parent 264c7488d532cd4f1425d94f1d74486c389cb118 tuned signature; diff -r 264c7488d532 -r 91c3aedbfc5e src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Tue Nov 03 17:41:13 2015 +0100 +++ b/src/Pure/Concurrent/future.scala Tue Nov 03 17:53:09 2015 +0100 @@ -8,6 +8,9 @@ package isabelle +import java.util.concurrent.Callable + + /* futures and promises */ object Future @@ -85,7 +88,7 @@ status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result)) } } - private val task = Standard_Thread.submit_task { try_run() } + private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body }) def join_result: Exn.Result[A] = { diff -r 264c7488d532 -r 91c3aedbfc5e src/Pure/Concurrent/standard_thread.scala --- a/src/Pure/Concurrent/standard_thread.scala Tue Nov 03 17:41:13 2015 +0100 +++ b/src/Pure/Concurrent/standard_thread.scala Tue Nov 03 17:53:09 2015 +0100 @@ -9,13 +9,14 @@ import java.lang.Thread -import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor, - TimeUnit, LinkedBlockingQueue} +import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue} + +import scala.concurrent.{ExecutionContext, ExecutionContextExecutor} object Standard_Thread { - /* plain thread */ + /* fork */ def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = { @@ -28,7 +29,7 @@ } - /* thread pool */ + /* pool */ lazy val pool: ThreadPoolExecutor = { @@ -37,8 +38,8 @@ new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) } - def submit_task[A](body: => A): JFuture[A] = - pool.submit(new Callable[A] { def call = body }) + lazy val execution_context: ExecutionContextExecutor = + ExecutionContext.fromExecutorService(pool) /* delayed events */