--- a/Admin/polyml/future/ROOT.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/Admin/polyml/future/ROOT.ML Tue Nov 03 18:11:59 2015 +0100
@@ -101,7 +101,7 @@
use "General/properties.ML";
use "General/timing.ML";
-use "Concurrent/simple_thread.ML";
+use "Concurrent/standard_thread.ML";
use "Concurrent/synchronized.ML";
use "General/markup.ML";
use "Concurrent/single_assignment.ML";
--- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue Nov 03 18:11:59 2015 +0100
@@ -5,7 +5,7 @@
section \<open>Complex Analysis Basics\<close>
theory Complex_Analysis_Basics
-imports "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space"
+imports Cartesian_Euclidean_Space
begin
--- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Nov 03 18:11:59 2015 +0100
@@ -5,7 +5,7 @@
section \<open>Complex Transcendental Functions\<close>
theory Complex_Transcendental
-imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
+imports Complex_Analysis_Basics
begin
lemma cmod_add_real_less:
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Tue Nov 03 18:11:59 2015 +0100
@@ -6,7 +6,7 @@
section \<open>Multivariate calculus in Euclidean space\<close>
theory Derivative
-imports Brouwer_Fixpoint Operator_Norm "~~/src/HOL/Multivariate_Analysis/Uniform_Limit"
+imports Brouwer_Fixpoint Operator_Norm Uniform_Limit
begin
lemma netlimit_at_vector: (* TODO: move *)
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Nov 03 18:11:59 2015 +0100
@@ -8,7 +8,10 @@
section \<open>Limits on the Extended real number line\<close>
theory Extended_Real_Limits
- imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
+imports
+ Topology_Euclidean_Space
+ "~~/src/HOL/Library/Extended_Real"
+ "~~/src/HOL/Library/Indicator_Function"
begin
lemma compact_UNIV:
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy Tue Nov 03 18:11:59 2015 +0100
@@ -1,12 +1,11 @@
-section \<open>polynomial functions: extremal behaviour and root counts\<close>
-
(* Author: John Harrison and Valentina Bruno
Ported from "hol_light/Multivariate/complexes.ml" by L C Paulson
*)
+section \<open>polynomial functions: extremal behaviour and root counts\<close>
+
theory PolyRoots
imports Complex_Main
-
begin
subsection\<open>Geometric progressions\<close>
--- a/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/Weierstrass.thy Tue Nov 03 18:11:59 2015 +0100
@@ -1,8 +1,7 @@
-section\<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
+section \<open>Bernstein-Weierstrass and Stone-Weierstrass Theorems\<close>
theory Weierstrass
imports Uniform_Limit Path_Connected
-
begin
(*FIXME: simplification changes to be enforced globally*)
--- a/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Multivariate_Analysis/ex/Approximations.thy Tue Nov 03 18:11:59 2015 +0100
@@ -1,7 +1,7 @@
section \<open>Binary Approximations to Constants\<close>
theory Approximations
-imports "~~/src/HOL/Multivariate_Analysis/Complex_Transcendental"
+imports Complex_Transcendental
begin
declare of_real_numeral [simp]
--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Tue Nov 03 18:11:59 2015 +0100
@@ -24,7 +24,7 @@
Runtime.debugging NONE body () handle exn =>
if Exn.is_interrupt exn then ()
else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
- Simple_Thread.attributes
+ Standard_Thread.attributes
{name = "async_manager", stack_limit = NONE, interrupts = interrupts});
fun implode_message (workers, work) =
@@ -108,7 +108,7 @@
NONE
else
let
- val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
+ val _ = List.app (Standard_Thread.interrupt_unsynchronized o #1) canceling
val canceling' = filter (Thread.isActive o #1) canceling
val state' = make_state manager timeout_heap' active canceling' messages
in SOME (map #2 timeout_threads, state') end
--- a/src/Pure/Concurrent/bash.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML Tue Nov 03 18:11:59 2015 +0100
@@ -31,7 +31,7 @@
val _ = cleanup_files ();
val system_thread =
- Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
@@ -83,7 +83,7 @@
in () end;
fun cleanup () =
- (Simple_Thread.interrupt_unsynchronized system_thread;
+ (Standard_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
in
let
--- a/src/Pure/Concurrent/bash_windows.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML Tue Nov 03 18:11:59 2015 +0100
@@ -35,7 +35,7 @@
val _ = cleanup_files ();
val system_thread =
- Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
@@ -74,7 +74,7 @@
in () end;
fun cleanup () =
- (Simple_Thread.interrupt_unsynchronized system_thread;
+ (Standard_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
in
let
--- a/src/Pure/Concurrent/consumer_thread.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala Tue Nov 03 18:11:59 2015 +0100
@@ -32,7 +32,7 @@
private var active = true
private val mailbox = Mailbox[Option[Consumer_Thread.Request[A]]]
- private val thread = Simple_Thread.fork(name, daemon) { main_loop(Nil) }
+ private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
def is_active: Boolean = active && thread.isAlive
private def failure(exn: Throwable): Unit =
--- a/src/Pure/Concurrent/event_timer.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Tue Nov 03 18:11:59 2015 +0100
@@ -105,7 +105,7 @@
fun manager_check manager =
if is_some manager andalso Thread.isActive (the manager) then manager
else
- SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
+ SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
manager_loop);
fun shutdown () =
--- a/src/Pure/Concurrent/future.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Nov 03 18:11:59 2015 +0100
@@ -184,14 +184,14 @@
let
val running = Task_Queue.cancel (! queue) group;
val _ = running |> List.app (fn thread =>
- if Simple_Thread.is_self thread then ()
- else Simple_Thread.interrupt_unsynchronized thread);
+ if Standard_Thread.is_self thread then ()
+ else Standard_Thread.interrupt_unsynchronized thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
let
val (groups, threads) = Task_Queue.cancel_all (! queue);
- val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+ val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
in groups end;
fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -264,7 +264,7 @@
Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
val worker =
- Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+ Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
(fn () => worker_loop name);
in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
@@ -367,7 +367,7 @@
if scheduler_active () then ()
else
scheduler :=
- SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+ SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
scheduler_loop));
--- a/src/Pure/Concurrent/future.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/future.scala Tue Nov 03 18:11:59 2015 +0100
@@ -2,31 +2,24 @@
Module: PIDE
Author: Makarius
-Value-oriented parallel execution via futures and promises in Scala -- with
-signatures as in Isabelle/ML.
+Value-oriented parallel execution via futures and promises.
*/
package isabelle
-import scala.util.{Success, Failure}
-import scala.concurrent.{ExecutionContext, ExecutionContextExecutor,
- Future => Scala_Future, Promise => Scala_Promise, Await}
-import scala.concurrent.duration.Duration
+import java.util.concurrent.Callable
+/* futures and promises */
+
object Future
{
- lazy val execution_context: ExecutionContextExecutor =
- ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
-
- def value[A](x: A): Future[A] = new Finished_Future(x)
-
- def fork[A](body: => A): Future[A] =
- new Pending_Future(Scala_Future[A](body)(execution_context))
-
- def promise[A]: Promise[A] =
- new Promise_Future[A](Scala_Promise[A]())
+ def value[A](x: A): Future[A] = new Value_Future(x)
+ def fork[A](body: => A): Future[A] = new Task_Future[A](body)
+ def promise[A]: Promise[A] = new Promise_Future[A]
+ def thread[A](name: String = "", daemon: Boolean = false)(body: => A): Future[A] =
+ new Thread_Future[A](name, daemon, body)
}
trait Future[A]
@@ -34,8 +27,10 @@
def peek: Option[Exn.Result[A]]
def is_finished: Boolean = peek.isDefined
def get_finished: A = { require(is_finished); Exn.release(peek.get) }
- def join: A
+ def join_result: Exn.Result[A]
+ def join: A = Exn.release(join_result)
def map[B](f: A => B): Future[B] = Future.fork { f(join) }
+ def cancel: Unit
override def toString: String =
peek match {
@@ -47,46 +42,103 @@
trait Promise[A] extends Future[A]
{
- def cancel: Unit
def fulfill_result(res: Exn.Result[A]): Unit
def fulfill(x: A): Unit
}
-private class Finished_Future[A](x: A) extends Future[A]
+/* value future */
+
+private class Value_Future[A](x: A) extends Future[A]
{
val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
- val join: A = x
+ def join_result: Exn.Result[A] = peek.get
+ def cancel {}
}
-private class Pending_Future[A](future: Scala_Future[A]) extends Future[A]
+
+/* task future via thread pool */
+
+private class Task_Future[A](body: => A) extends Future[A]
{
+ private sealed abstract class Status
+ private case object Ready extends Status
+ private case class Running(thread: Thread) extends Status
+ private case object Terminated extends Status
+ private case class Finished(result: Exn.Result[A]) extends Status
+
+ private val status = Synchronized[Status](Ready)
+
def peek: Option[Exn.Result[A]] =
- future.value match {
- case Some(Success(x)) => Some(Exn.Res(x))
- case Some(Failure(e)) => Some(Exn.Exn(e))
- case None => None
+ status.value match {
+ case Finished(result) => Some(result)
+ case _ => None
+ }
+
+ private def try_run()
+ {
+ val do_run =
+ status.change_result {
+ case Ready => (true, Running(Thread.currentThread))
+ case st => (false, st)
+ }
+ if (do_run) {
+ val result = Exn.capture(body)
+ status.change(_ => Terminated)
+ status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
}
- override def is_finished: Boolean = future.isCompleted
+ }
+ private val task = Standard_Thread.pool.submit(new Callable[A] { def call = body })
- def join: A = Await.result(future, Duration.Inf)
- override def map[B](f: A => B): Future[B] =
- new Pending_Future[B](future.map(f)(Future.execution_context))
+ def join_result: Exn.Result[A] =
+ {
+ try_run()
+ status.guarded_access {
+ case st @ Finished(result) => Some((result, st))
+ case _ => None
+ }
+ }
+
+ def cancel =
+ {
+ status.change {
+ case Ready => task.cancel(false); Finished(Exn.Exn(Exn.Interrupt()))
+ case st @ Running(thread) => thread.interrupt; st
+ case st => st
+ }
+ }
}
-private class Promise_Future[A](promise: Scala_Promise[A])
- extends Pending_Future(promise.future) with Promise[A]
+
+/* promise future */
+
+private class Promise_Future[A] extends Promise[A]
{
- override def is_finished: Boolean = promise.isCompleted
+ private val state = Synchronized[Option[Exn.Result[A]]](None)
+ def peek: Option[Exn.Result[A]] = state.value
+
+ def join_result: Exn.Result[A] =
+ state.guarded_access(st => if (st.isEmpty) None else Some((st.get, st)))
+
+ def fulfill_result(result: Exn.Result[A]): Unit =
+ state.change(st => if (st.isEmpty) Some(result) else throw new IllegalStateException)
+
+ def fulfill(x: A): Unit = fulfill_result(Exn.Res(x))
def cancel: Unit =
- try { fulfill_result(Exn.Exn(Exn.Interrupt())) }
- catch { case _: IllegalStateException => }
+ state.change(st => if (st.isEmpty) Some(Exn.Exn(Exn.Interrupt())) else st)
+}
+
+
+/* thread future */
- def fulfill_result(res: Exn.Result[A]): Unit =
- res match {
- case Exn.Res(x) => promise.success(x)
- case Exn.Exn(e) => promise.failure(e)
- }
- def fulfill(x: A): Unit = promise.success(x)
+private class Thread_Future[A](name: String, daemon: Boolean, body: => A) extends Future[A]
+{
+ private val result = Future.promise[A]
+ private val thread =
+ Standard_Thread.fork(name, daemon) { result.fulfill_result(Exn.capture(body)) }
+
+ def peek: Option[Exn.Result[A]] = result.peek
+ def join_result: Exn.Result[A] = result.join_result
+ def cancel: Unit = thread.interrupt
}
--- a/src/Pure/Concurrent/par_list.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala Tue Nov 03 18:11:59 2015 +0100
@@ -8,38 +8,34 @@
package isabelle
-import java.util.concurrent.{Future => JFuture, CancellationException}
-
-
object Par_List
{
def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
else {
- val state = Synchronized((List.empty[JFuture[Exn.Result[B]]], false))
+ val state = Synchronized((List.empty[Future[B]], false))
def cancel_other(self: Int = -1): Unit =
- state.change { case (tasks, canceled) =>
+ state.change { case (futures, canceled) =>
if (!canceled) {
- for ((task, i) <- tasks.iterator.zipWithIndex if i != self)
- task.cancel(true)
+ for ((future, i) <- futures.iterator.zipWithIndex if i != self)
+ future.cancel
}
- (tasks, true)
+ (futures, true)
}
try {
state.change(_ =>
(xs.iterator.zipWithIndex.map({ case (x, self) =>
- Simple_Thread.submit_task {
- val result = Exn.capture { f(x) }
- result match { case Exn.Exn(_) => cancel_other(self) case _ => }
- result
+ Future.fork {
+ Exn.capture { f(x) } match {
+ case Exn.Exn(exn) => cancel_other(self); throw exn
+ case Exn.Res(res) => res
+ }
}
}).toList, false))
- state.value._1.map(future =>
- try { future.get }
- catch { case _: CancellationException => Exn.Exn(Exn.Interrupt()): Exn.Result[B] })
+ state.value._1.map(_.join_result)
}
finally { cancel_other() }
}
@@ -65,4 +61,3 @@
def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
}
-
--- a/src/Pure/Concurrent/simple_thread.ML Tue Nov 03 15:24:24 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(* Title: Pure/Concurrent/simple_thread.ML
- Author: Makarius
-
-Simplified thread operations.
-*)
-
-signature SIMPLE_THREAD =
-sig
- val is_self: Thread.thread -> bool
- val get_name: unit -> string option
- val the_name: unit -> string
- type params = {name: string, stack_limit: int option, interrupts: bool}
- val attributes: params -> Thread.threadAttribute list
- val fork: params -> (unit -> unit) -> Thread.thread
- val join: Thread.thread -> unit
- val interrupt_unsynchronized: Thread.thread -> unit
-end;
-
-structure Simple_Thread: SIMPLE_THREAD =
-struct
-
-(* self *)
-
-fun is_self thread = Thread.equal (Thread.self (), thread);
-
-
-(* unique name *)
-
-local
- val tag = Universal.tag () : string Universal.tag;
- val count = Counter.make ();
-in
-
-fun get_name () = Thread.getLocal tag;
-
-fun the_name () =
- (case get_name () of
- NONE => raise Fail "Unknown thread name"
- | SOME name => name);
-
-fun set_name base =
- Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
-
-end;
-
-
-(* fork *)
-
-type params = {name: string, stack_limit: int option, interrupts: bool};
-
-fun attributes ({stack_limit, interrupts, ...}: params) =
- ML_Stack.limit stack_limit @
- (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
-
-fun fork (params: params) body =
- Thread.fork (fn () =>
- print_exception_trace General.exnMessage tracing (fn () =>
- (set_name (#name params); body ())
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
- attributes params);
-
-
-(* join *)
-
-fun join thread =
- while Thread.isActive thread
- do OS.Process.sleep (seconds 0.1);
-
-
-(* interrupt *)
-
-fun interrupt_unsynchronized thread =
- Thread.interrupt thread handle Thread _ => ();
-
-end;
--- a/src/Pure/Concurrent/simple_thread.scala Tue Nov 03 15:24:24 2015 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,110 +0,0 @@
-/* Title: Pure/Concurrent/simple_thread.scala
- Module: PIDE
- Author: Makarius
-
-Simplified thread operations.
-*/
-
-package isabelle
-
-
-import java.lang.Thread
-import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
- TimeUnit, LinkedBlockingQueue}
-
-
-object Simple_Thread
-{
- /* plain thread */
-
- def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
- {
- val thread =
- if (name == null || name == "") new Thread() { override def run = body }
- else new Thread(name) { override def run = body }
- thread.setDaemon(daemon)
- thread.start
- thread
- }
-
-
- /* 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 =
- {
- 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
- new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
- }
-
- def submit_task[A](body: => A): JFuture[A] =
- default_pool.submit(new Callable[A] { def call = body })
-
-
- /* delayed events */
-
- final class Delay private [Simple_Thread](
- first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
- {
- private var running: Option[Event_Timer.Request] = None
-
- private def run: Unit =
- {
- val do_run = synchronized {
- if (running.isDefined) { running = None; true } else false
- }
- if (do_run) event
- }
-
- def invoke(): Unit = synchronized
- {
- val new_run =
- running match {
- case Some(request) => if (first) false else { request.cancel; cancel(); true }
- case None => true
- }
- if (new_run)
- running = Some(Event_Timer.request(Time.now() + delay)(run))
- }
-
- def revoke(): Unit = synchronized
- {
- running match {
- case Some(request) => request.cancel; cancel(); running = None
- case None => cancel()
- }
- }
-
- def postpone(alt_delay: Time): Unit = synchronized
- {
- running match {
- case Some(request) =>
- val alt_time = Time.now() + alt_delay
- if (request.time < alt_time && request.cancel) {
- cancel()
- running = Some(Event_Timer.request(alt_time)(run))
- }
- else cancel()
- case None => cancel()
- }
- }
- }
-
- // delayed event after first invocation
- def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
- new Delay(true, delay, cancel, event)
-
- // delayed event after last invocation
- def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
- new Delay(false, delay, cancel, event)
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/standard_thread.ML Tue Nov 03 18:11:59 2015 +0100
@@ -0,0 +1,75 @@
+(* Title: Pure/Concurrent/standard_thread.ML
+ Author: Makarius
+
+Standard thread operations.
+*)
+
+signature STANDARD_THREAD =
+sig
+ val is_self: Thread.thread -> bool
+ val get_name: unit -> string option
+ val the_name: unit -> string
+ type params = {name: string, stack_limit: int option, interrupts: bool}
+ val attributes: params -> Thread.threadAttribute list
+ val fork: params -> (unit -> unit) -> Thread.thread
+ val join: Thread.thread -> unit
+ val interrupt_unsynchronized: Thread.thread -> unit
+end;
+
+structure Standard_Thread: STANDARD_THREAD =
+struct
+
+(* self *)
+
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
+
+(* unique name *)
+
+local
+ val tag = Universal.tag () : string Universal.tag;
+ val count = Counter.make ();
+in
+
+fun get_name () = Thread.getLocal tag;
+
+fun the_name () =
+ (case get_name () of
+ NONE => raise Fail "Unknown thread name"
+ | SOME name => name);
+
+fun set_name base =
+ Thread.setLocal (tag, base ^ "/" ^ string_of_int (count ()));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
+ ML_Stack.limit stack_limit @
+ (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+
+fun fork (params: params) body =
+ Thread.fork (fn () =>
+ print_exception_trace General.exnMessage tracing (fn () =>
+ (set_name (#name params); body ())
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
+ attributes params);
+
+
+(* join *)
+
+fun join thread =
+ while Thread.isActive thread
+ do OS.Process.sleep (seconds 0.1);
+
+
+(* interrupt *)
+
+fun interrupt_unsynchronized thread =
+ Thread.interrupt thread handle Thread _ => ();
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/standard_thread.scala Tue Nov 03 18:11:59 2015 +0100
@@ -0,0 +1,101 @@
+/* Title: Pure/Concurrent/standard_thread.scala
+ Module: PIDE
+ Author: Makarius
+
+Standard thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue}
+
+import scala.concurrent.{ExecutionContext, ExecutionContextExecutor}
+
+
+object Standard_Thread
+{
+ /* fork */
+
+ def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
+ {
+ val thread =
+ if (name == null || name == "") new Thread() { override def run = body }
+ else new Thread(name) { override def run = body }
+ thread.setDaemon(daemon)
+ thread.start
+ thread
+ }
+
+
+ /* 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
+ new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+ }
+
+ lazy val execution_context: ExecutionContextExecutor =
+ ExecutionContext.fromExecutorService(pool)
+
+
+ /* delayed events */
+
+ final class Delay private [Standard_Thread](
+ first: Boolean, delay: => Time, cancel: () => Unit, event: => Unit)
+ {
+ private var running: Option[Event_Timer.Request] = None
+
+ private def run: Unit =
+ {
+ val do_run = synchronized {
+ if (running.isDefined) { running = None; true } else false
+ }
+ if (do_run) event
+ }
+
+ def invoke(): Unit = synchronized
+ {
+ val new_run =
+ running match {
+ case Some(request) => if (first) false else { request.cancel; cancel(); true }
+ case None => cancel(); true
+ }
+ if (new_run)
+ running = Some(Event_Timer.request(Time.now() + delay)(run))
+ }
+
+ def revoke(): Unit = synchronized
+ {
+ running match {
+ case Some(request) => request.cancel; cancel(); running = None
+ case None => cancel()
+ }
+ }
+
+ def postpone(alt_delay: Time): Unit = synchronized
+ {
+ running match {
+ case Some(request) =>
+ val alt_time = Time.now() + alt_delay
+ if (request.time < alt_time && request.cancel) {
+ cancel()
+ running = Some(Event_Timer.request(alt_time)(run))
+ }
+ else cancel()
+ case None => cancel()
+ }
+ }
+ }
+
+ // delayed event after first invocation
+ def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+ new Delay(true, delay, cancel, event)
+
+ // delayed event after last invocation
+ def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit): Delay =
+ new Delay(false, delay, cancel, event)
+}
--- a/src/Pure/Concurrent/time_limit.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Concurrent/time_limit.ML Tue Nov 03 18:11:59 2015 +0100
@@ -22,7 +22,7 @@
val request =
Event_Timer.request (Time.+ (Time.now (), timeout))
- (fn () => Simple_Thread.interrupt_unsynchronized self);
+ (fn () => Standard_Thread.interrupt_unsynchronized self);
val result =
Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
--- a/src/Pure/GUI/gui_thread.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/GUI/gui_thread.scala Tue Nov 03 18:11:59 2015 +0100
@@ -50,8 +50,8 @@
/* delayed events */
def delay_first(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
- : Simple_Thread.Delay = Simple_Thread.delay_first(delay, cancel) { later { event } }
+ : Standard_Thread.Delay = Standard_Thread.delay_first(delay, cancel) { later { event } }
def delay_last(delay: => Time, cancel: () => Unit = () => ())(event: => Unit)
- : Simple_Thread.Delay = Simple_Thread.delay_last(delay, cancel) { later { event } }
+ : Standard_Thread.Delay = Standard_Thread.delay_last(delay, cancel) { later { event } }
}
--- a/src/Pure/General/exn.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/General/exn.scala Tue Nov 03 18:11:59 2015 +0100
@@ -58,7 +58,7 @@
def apply(): Throwable = new InterruptedException
def unapply(exn: Throwable): Boolean = is_interrupt(exn)
- def expose() { if (Thread.interrupted()) throw apply() }
+ def expose() { if (Thread.interrupted) throw apply() }
def impose() { Thread.currentThread.interrupt }
def postpone[A](body: => A): Option[A] =
@@ -104,4 +104,3 @@
def message(exn: Throwable): String =
user_message(exn) getOrElse (if (is_interrupt(exn)) "Interrupt" else exn.toString)
}
-
--- a/src/Pure/PIDE/prover.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/PIDE/prover.scala Tue Nov 03 18:11:59 2015 +0100
@@ -121,8 +121,8 @@
/** process manager **/
- private val (_, process_result) =
- Simple_Thread.future("process_result") { system_process.join }
+ private val process_result =
+ Future.thread("process_result") { system_process.join }
private def terminate_process()
{
@@ -132,7 +132,7 @@
}
}
- private val process_manager = Simple_Thread.fork("process_manager")
+ private val process_manager = Standard_Thread.fork("process_manager")
{
val (startup_failed, startup_errors) =
{
@@ -230,7 +230,7 @@
if (err) ("standard_error", system_process.stderr, Markup.STDERR)
else ("standard_output", system_process.stdout, Markup.STDOUT)
- Simple_Thread.fork(name) {
+ Standard_Thread.fork(name) {
try {
var result = new StringBuilder(100)
var finished = false
@@ -268,7 +268,7 @@
class Protocol_Error(msg: String) extends Exception(msg)
val name = "message_output"
- Simple_Thread.fork(name) {
+ Standard_Thread.fork(name) {
val default_buffer = new Array[Byte](65536)
var c = -1
--- a/src/Pure/PIDE/session.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/PIDE/session.scala Tue Nov 03 18:11:59 2015 +0100
@@ -291,7 +291,7 @@
nodes = Set.empty
commands = Set.empty
}
- private val delay_flush = Simple_Thread.delay_first(output_delay) { flush() }
+ private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
def invoke(assign: Boolean, cmds: List[Command]): Unit = synchronized {
assignment |= assign
@@ -353,7 +353,7 @@
/* manager thread */
- private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+ private val delay_prune = Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
private val manager: Consumer_Thread[Any] =
{
--- a/src/Pure/ROOT Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/ROOT Tue Nov 03 18:11:59 2015 +0100
@@ -86,9 +86,9 @@
"Concurrent/par_list.ML"
"Concurrent/par_list_sequential.ML"
"Concurrent/random.ML"
- "Concurrent/simple_thread.ML"
"Concurrent/single_assignment.ML"
"Concurrent/single_assignment_sequential.ML"
+ "Concurrent/standard_thread.ML"
"Concurrent/synchronized.ML"
"Concurrent/synchronized_sequential.ML"
"Concurrent/task_queue.ML"
--- a/src/Pure/ROOT.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/ROOT.ML Tue Nov 03 18:11:59 2015 +0100
@@ -109,7 +109,7 @@
then use "ML/ml_statistics_polyml-5.5.0.ML"
else use "ML/ml_statistics_dummy.ML";
-use "Concurrent/simple_thread.ML";
+use "Concurrent/standard_thread.ML";
use "Concurrent/single_assignment.ML";
if Multithreading.available then ()
--- a/src/Pure/System/invoke_scala.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/invoke_scala.scala Tue Nov 03 18:11:59 2015 +0100
@@ -8,7 +8,6 @@
import java.lang.reflect.{Method, Modifier, InvocationTargetException}
-import java.util.concurrent.{Future => JFuture}
import scala.util.matching.Regex
@@ -72,7 +71,7 @@
class Invoke_Scala extends Session.Protocol_Handler
{
- private var futures = Map.empty[String, JFuture[Unit]]
+ private var futures = Map.empty[String, Future[Unit]]
private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
synchronized
@@ -83,9 +82,9 @@
}
}
- private def cancel(prover: Prover, id: String, future: JFuture[Unit])
+ private def cancel(prover: Prover, id: String, future: Future[Unit])
{
- future.cancel(true)
+ future.cancel
fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
}
@@ -94,7 +93,7 @@
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
futures += (id ->
- Simple_Thread.submit_task {
+ Future.fork {
val (tag, result) = Invoke_Scala.method(name, msg.text)
fulfill(prover, id, tag, result)
})
--- a/src/Pure/System/isabelle_system.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Nov 03 18:11:59 2015 +0100
@@ -328,14 +328,10 @@
proc.stdin.close
val limited = new Limited_Progress(proc, progress_limit)
- val (_, stdout) =
- Simple_Thread.future("bash_stdout") {
- File.read_lines(proc.stdout, limited(progress_stdout))
- }
- val (_, stderr) =
- Simple_Thread.future("bash_stderr") {
- File.read_lines(proc.stderr, limited(progress_stderr))
- }
+ val stdout =
+ Future.thread("bash_stdout") { File.read_lines(proc.stdout, limited(progress_stdout)) }
+ val stderr =
+ Future.thread("bash_stderr") { File.read_lines(proc.stderr, limited(progress_stderr)) }
val rc =
try { proc.join }
--- a/src/Pure/System/message_channel.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/System/message_channel.ML Tue Nov 03 18:11:59 2015 +0100
@@ -60,11 +60,11 @@
let
val mbox = Mailbox.create ();
val thread =
- Simple_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+ Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
(message_output mbox channel);
fun send msg = Mailbox.send mbox (SOME msg);
fun shutdown () =
- (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
+ (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
in Message_Channel {send = send, shutdown = shutdown} end
else
let
--- a/src/Pure/Tools/build.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 03 18:11:59 2015 +0100
@@ -598,8 +598,8 @@
"""
}
- private val (thread, result) =
- Simple_Thread.future("build") {
+ private val result =
+ Future.thread("build") {
Isabelle_System.bash_env(info.dir.file, env, script,
progress_stdout = (line: String) =>
Library.try_unprefix("\floading_theory = ", line) match {
@@ -614,7 +614,7 @@
strict = false)
}
- def terminate: Unit = thread.interrupt
+ def terminate: Unit = result.cancel
def is_finished: Boolean = result.is_finished
@volatile private var was_timeout = false
--- a/src/Pure/Tools/debugger.ML Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/debugger.ML Tue Nov 03 18:11:59 2015 +0100
@@ -24,7 +24,7 @@
if msg = "" then ()
else
Output.protocol_message
- (Markup.debugger_output (Simple_Thread.the_name ()))
+ (Markup.debugger_output (Standard_Thread.the_name ()))
[Markup.markup (kind, Markup.serial_properties (serial ())) msg];
val writeln_message = output_message Markup.writelnN;
@@ -255,7 +255,7 @@
(SOME (fn (_, break) =>
if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
then
- (case Simple_Thread.get_name () of
+ (case Standard_Thread.get_name () of
SOME thread_name => debugger_loop thread_name
| NONE => ())
else ()))));
--- a/src/Pure/Tools/debugger.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/Tools/debugger.scala Tue Nov 03 18:11:59 2015 +0100
@@ -114,7 +114,7 @@
case object Update
private val delay_update =
- Simple_Thread.delay_first(global_state.value.session.output_delay) {
+ Standard_Thread.delay_first(global_state.value.session.output_delay) {
global_state.value.session.debugger_updates.post(Update)
}
--- a/src/Pure/build-jars Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Pure/build-jars Tue Nov 03 18:11:59 2015 +0100
@@ -16,7 +16,7 @@
Concurrent/future.scala
Concurrent/mailbox.scala
Concurrent/par_list.scala
- Concurrent/simple_thread.scala
+ Concurrent/standard_thread.scala
Concurrent/synchronized.scala
GUI/color_value.scala
GUI/gui.scala
--- a/src/Tools/jEdit/src/active.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/active.scala Tue Nov 03 18:11:59 2015 +0100
@@ -30,7 +30,7 @@
// FIXME avoid hard-wired stuff
elem match {
case XML.Elem(Markup(Markup.BROWSER, _), body) =>
- Future.fork {
+ Standard_Thread.fork("browser") {
val graph_file = Isabelle_System.tmp_file("graph")
File.write(graph_file, XML.content(body))
Isabelle_System.bash_env(null,
@@ -39,7 +39,7 @@
}
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
- Future.fork {
+ Standard_Thread.fork("graphview") {
val graph =
Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Nov 03 18:11:59 2015 +0100
@@ -59,7 +59,7 @@
if (path.is_file)
PIDE.editor.goto_file(true, view, File.platform_path(path))
else {
- Future.fork {
+ Standard_Thread.fork("documentation") {
try { Doc.view(path) }
catch {
case exn: Throwable =>
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Nov 03 18:11:59 2015 +0100
@@ -194,7 +194,7 @@
new Hyperlink {
val external = true
def follow(view: View): Unit =
- Future.fork {
+ Standard_Thread.fork("hyperlink_url") {
try { Isabelle_System.open(name) }
catch {
case exn: Throwable =>
--- a/src/Tools/jEdit/src/pretty_text_area.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Nov 03 18:11:59 2015 +0100
@@ -10,7 +10,6 @@
import isabelle._
-import java.util.concurrent.{Future => JFuture}
import java.awt.{Color, Font, Toolkit, Window}
import java.awt.event.KeyEvent
import javax.swing.JTextField
@@ -75,7 +74,7 @@
private var current_base_results = Command.Results.empty
private var current_rendering: Rendering =
Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
- private var future_refresh: Option[JFuture[Unit]] = None
+ private var future_refresh: Option[Future[Unit]] = None
private val rich_text_area =
new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
@@ -128,9 +127,9 @@
val base_results = current_base_results
val formatted_body = Pretty.formatted(current_body, margin, metric)
- future_refresh.map(_.cancel(true))
+ future_refresh.map(_.cancel)
future_refresh =
- Some(Simple_Thread.submit_task {
+ Some(Future.fork {
val (text, rendering) =
try { Pretty_Text_Area.text_rendering(base_snapshot, base_results, formatted_body) }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
--- a/src/Tools/jEdit/src/scala_console.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Tue Nov 03 18:11:59 2015 +0100
@@ -165,7 +165,7 @@
}
finally {
running.change(_ => None)
- Thread.interrupted()
+ Thread.interrupted
}
GUI_Thread.later {
if (err != null) err.commandDone()
--- a/src/Tools/jEdit/src/session_build.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Tue Nov 03 18:11:59 2015 +0100
@@ -161,7 +161,7 @@
setLocationRelativeTo(view)
setVisible(true)
- Simple_Thread.fork("session_build") {
+ Standard_Thread.fork("session_build") {
progress.echo("Build started for Isabelle/" + Isabelle_Logic.session_name() + " ...")
val (out, rc) =
--- a/src/Tools/jEdit/src/text_overview.scala Tue Nov 03 15:24:24 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Tue Nov 03 18:11:59 2015 +0100
@@ -11,7 +11,6 @@
import scala.annotation.tailrec
-import java.util.concurrent.{Future => JFuture}
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color}
import java.awt.event.{MouseAdapter, MouseEvent}
import javax.swing.{JPanel, ToolTipManager}
@@ -102,8 +101,8 @@
/* asynchronous refresh */
- private var future_refresh: Option[JFuture[Unit]] = None
- private def cancel(): Unit = future_refresh.map(_.cancel(true))
+ private var future_refresh: Option[Future[Unit]] = None
+ private def cancel(): Unit = future_refresh.map(_.cancel)
def invoke(): Unit = delay_refresh.invoke()
def revoke(): Unit = delay_refresh.revoke()
@@ -128,7 +127,7 @@
}
future_refresh =
- Some(Simple_Thread.submit_task {
+ Some(Future.fork {
val line_count = overview.line_count
val char_count = overview.char_count
val L = overview.L