--- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Sun Apr 05 13:05:40 2020 +0200
@@ -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),
- Standard_Thread.attributes
+ Isabelle_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 (Standard_Thread.interrupt_unsynchronized o #1) canceling
+ val _ = List.app (Isabelle_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/consumer_thread.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala Sun Apr 05 13:05:40 2020 +0200
@@ -47,7 +47,7 @@
private var active = true
private val mailbox = Mailbox[Option[Request]]
- private val thread = Standard_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
+ private val thread = Isabelle_Thread.fork(name = name, daemon = daemon) { main_loop(Nil) }
def is_active: Boolean = active && thread.isAlive
def check_thread: Boolean = Thread.currentThread == thread
--- a/src/Pure/Concurrent/event_timer.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Sun Apr 05 13:05:40 2020 +0200
@@ -130,7 +130,7 @@
fun manager_check manager =
if is_some manager andalso Thread.isActive (the manager) then manager
else
- SOME (Standard_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
+ SOME (Isabelle_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
manager_loop);
fun shutdown () =
--- a/src/Pure/Concurrent/future.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/future.ML Sun Apr 05 13:05:40 2020 +0200
@@ -202,14 +202,14 @@
let
val running = Task_Queue.cancel (! queue) group;
val _ = running |> List.app (fn thread =>
- if Standard_Thread.is_self thread then ()
- else Standard_Thread.interrupt_unsynchronized thread);
+ if Isabelle_Thread.is_self thread then ()
+ else Isabelle_Thread.interrupt_unsynchronized thread);
in running end;
fun cancel_all () = (*requires SYNCHRONIZED*)
let
val (groups, threads) = Task_Queue.cancel_all (! queue);
- val _ = List.app Standard_Thread.interrupt_unsynchronized threads;
+ val _ = List.app Isabelle_Thread.interrupt_unsynchronized threads;
in groups end;
fun cancel_later group = (*requires SYNCHRONIZED*)
@@ -280,7 +280,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 =
- Standard_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
+ Isabelle_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);
@@ -383,7 +383,7 @@
if scheduler_active () then ()
else
scheduler :=
- SOME (Standard_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
+ SOME (Isabelle_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
scheduler_loop));
--- a/src/Pure/Concurrent/future.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/future.scala Sun Apr 05 13:05:40 2020 +0200
@@ -20,7 +20,7 @@
def thread[A](
name: String = "",
- group: ThreadGroup = Standard_Thread.current_thread_group,
+ group: ThreadGroup = Isabelle_Thread.current_thread_group,
pri: Int = Thread.NORM_PRIORITY,
daemon: Boolean = false,
inherit_locals: Boolean = false,
@@ -96,7 +96,7 @@
status.change(_ => Finished(if (Thread.interrupted) Exn.Exn(Exn.Interrupt()) else result))
}
}
- private val task = Standard_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
+ private val task = Isabelle_Thread.pool.submit(new Callable[Unit] { def call = try_run() })
def join_result: Exn.Result[A] =
{
@@ -151,7 +151,7 @@
{
private val result = Future.promise[A]
private val thread =
- Standard_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
+ Isabelle_Thread.fork(name = name, group = group, pri = pri, daemon = daemon,
inherit_locals = inherit_locals, uninterruptible = uninterruptible)
{ result.fulfill_result(Exn.capture(body)) }
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/isabelle_thread.ML Sun Apr 05 13:05:40 2020 +0200
@@ -0,0 +1,76 @@
+(* Title: Pure/Concurrent/isabelle_thread.ML
+ Author: Makarius
+
+Isabelle-specific thread management.
+*)
+
+signature ISABELLE_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 Isabelle_Thread: ISABELLE_THREAD =
+struct
+
+(* self *)
+
+fun is_self thread = Thread.equal (Thread.self (), thread);
+
+
+(* unique name *)
+
+local
+ val name_var = Thread_Data.var () : string Thread_Data.var;
+ val count = Counter.make ();
+in
+
+fun get_name () = Thread_Data.get name_var;
+
+fun the_name () =
+ (case get_name () of
+ NONE => raise Fail "Unknown thread name"
+ | SOME name => name);
+
+fun set_name base =
+ Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
+
+end;
+
+
+(* fork *)
+
+type params = {name: string, stack_limit: int option, interrupts: bool};
+
+fun attributes ({stack_limit, interrupts, ...}: params) =
+ Thread.MaximumMLStack stack_limit ::
+ Thread_Attributes.convert_attributes
+ (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+
+fun fork (params: params) body =
+ Thread.fork (fn () =>
+ Exn.trace General.exnMessage tracing (fn () =>
+ (set_name (#name params); body ())
+ handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.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/isabelle_thread.scala Sun Apr 05 13:05:40 2020 +0200
@@ -0,0 +1,169 @@
+/* Title: Pure/Concurrent/isabelle_thread.scala
+ Author: Makarius
+
+Isabelle-specific thread management.
+*/
+
+package isabelle
+
+
+import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
+
+
+object Isabelle_Thread
+{
+ /* fork */
+
+ private val counter = Counter.make()
+
+ def make_name(name: String = "", base: String = "thread"): String =
+ proper_string(name).getOrElse(base + counter())
+
+ def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
+
+ def fork(
+ name: String = "",
+ group: ThreadGroup = current_thread_group,
+ pri: Int = Thread.NORM_PRIORITY,
+ daemon: Boolean = false,
+ inherit_locals: Boolean = false,
+ uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread =
+ {
+ val main =
+ if (uninterruptible) new Runnable { override def run { Isabelle_Thread.uninterruptible { body } } }
+ else new Runnable { override def run { body } }
+ val thread =
+ new Isabelle_Thread(main, name = make_name(name = name), group = group,
+ pri = pri, daemon = daemon, inherit_locals = inherit_locals)
+ thread.start
+ thread
+ }
+
+
+ /* self */
+
+ def self: Isabelle_Thread =
+ Thread.currentThread match {
+ case thread: Isabelle_Thread => thread
+ case _ => error("Expected to run on Isabelle/Scala standard thread")
+ }
+
+ def uninterruptible[A](body: => A): A = self.uninterruptible(body)
+
+
+ /* pool */
+
+ lazy val pool: ThreadPoolExecutor =
+ {
+ val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+ val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+ val executor =
+ new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+ executor.setThreadFactory(
+ new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
+ executor
+ }
+
+
+ /* delayed events */
+
+ final class Delay private[Isabelle_Thread](
+ first: Boolean, delay: => Time, log: Logger, 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) {
+ try { event }
+ catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
+ }
+ }
+
+ def invoke(): Unit = synchronized
+ {
+ val new_run =
+ running match {
+ case Some(request) => if (first) false else { request.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; running = None
+ case None =>
+ }
+ }
+
+ 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) {
+ running = Some(Event_Timer.request(alt_time)(run))
+ }
+ case None =>
+ }
+ }
+ }
+
+ // delayed event after first invocation
+ def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
+ new Delay(true, delay, log, event)
+
+ // delayed event after last invocation
+ def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
+ new Delay(false, delay, log, event)
+}
+
+class Isabelle_Thread private(
+ main: Runnable,
+ name: String = "",
+ group: ThreadGroup = null,
+ pri: Int = Thread.NORM_PRIORITY,
+ daemon: Boolean = false,
+ inherit_locals: Boolean = false)
+ extends Thread(group, null, name, 0L, inherit_locals)
+{
+ thread =>
+
+ thread.setPriority(pri)
+ thread.setDaemon(daemon)
+
+ override def run { main.run() }
+
+ private var interruptible: Boolean = true
+ private var interrupt_pending: Boolean = false
+
+ override def interrupt: Unit = synchronized
+ {
+ if (interruptible) super.interrupt()
+ else { interrupt_pending = true }
+ }
+
+ def uninterruptible[A](body: => A): A =
+ {
+ require(Thread.currentThread == thread)
+
+ val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
+ try { body }
+ finally {
+ synchronized {
+ interruptible = interruptible0
+ if (interruptible && interrupt_pending) {
+ interrupt_pending = false
+ super.interrupt()
+ }
+ }
+ Exn.Interrupt.expose()
+ }
+ }
+}
--- a/src/Pure/Concurrent/standard_thread.ML Sat Apr 04 21:38:20 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,76 +0,0 @@
-(* 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 name_var = Thread_Data.var () : string Thread_Data.var;
- val count = Counter.make ();
-in
-
-fun get_name () = Thread_Data.get name_var;
-
-fun the_name () =
- (case get_name () of
- NONE => raise Fail "Unknown thread name"
- | SOME name => name);
-
-fun set_name base =
- Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
-
-end;
-
-
-(* fork *)
-
-type params = {name: string, stack_limit: int option, interrupts: bool};
-
-fun attributes ({stack_limit, interrupts, ...}: params) =
- Thread.MaximumMLStack stack_limit ::
- Thread_Attributes.convert_attributes
- (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
-
-fun fork (params: params) body =
- Thread.fork (fn () =>
- Exn.trace General.exnMessage tracing (fn () =>
- (set_name (#name params); body ())
- handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.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/standard_thread.scala Sat Apr 04 21:38:20 2020 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,169 +0,0 @@
-/* Title: Pure/Concurrent/standard_thread.scala
- Author: Makarius
-
-Standard thread operations.
-*/
-
-package isabelle
-
-
-import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory}
-
-
-object Standard_Thread
-{
- /* fork */
-
- private val counter = Counter.make()
-
- def make_name(name: String = "", base: String = "thread"): String =
- proper_string(name).getOrElse(base + counter())
-
- def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup
-
- def fork(
- name: String = "",
- group: ThreadGroup = current_thread_group,
- pri: Int = Thread.NORM_PRIORITY,
- daemon: Boolean = false,
- inherit_locals: Boolean = false,
- uninterruptible: Boolean = false)(body: => Unit): Standard_Thread =
- {
- val main =
- if (uninterruptible) new Runnable { override def run { Standard_Thread.uninterruptible { body } } }
- else new Runnable { override def run { body } }
- val thread =
- new Standard_Thread(main, name = make_name(name = name), group = group,
- pri = pri, daemon = daemon, inherit_locals = inherit_locals)
- thread.start
- thread
- }
-
-
- /* self */
-
- def self: Standard_Thread =
- Thread.currentThread match {
- case thread: Standard_Thread => thread
- case _ => error("Expected to run on Isabelle/Scala standard thread")
- }
-
- def uninterruptible[A](body: => A): A = self.uninterruptible(body)
-
-
- /* pool */
-
- lazy val pool: ThreadPoolExecutor =
- {
- val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
- val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
- val executor =
- new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
- executor.setThreadFactory(
- new Standard_Thread(_, name = make_name(base = "worker"), group = current_thread_group))
- executor
- }
-
-
- /* delayed events */
-
- final class Delay private[Standard_Thread](
- first: Boolean, delay: => Time, log: Logger, 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) {
- try { event }
- catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn }
- }
- }
-
- def invoke(): Unit = synchronized
- {
- val new_run =
- running match {
- case Some(request) => if (first) false else { request.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; running = None
- case None =>
- }
- }
-
- 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) {
- running = Some(Event_Timer.request(alt_time)(run))
- }
- case None =>
- }
- }
- }
-
- // delayed event after first invocation
- def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(true, delay, log, event)
-
- // delayed event after last invocation
- def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay =
- new Delay(false, delay, log, event)
-}
-
-class Standard_Thread private(
- main: Runnable,
- name: String = "",
- group: ThreadGroup = null,
- pri: Int = Thread.NORM_PRIORITY,
- daemon: Boolean = false,
- inherit_locals: Boolean = false)
- extends Thread(group, null, name, 0L, inherit_locals)
-{
- thread =>
-
- thread.setPriority(pri)
- thread.setDaemon(daemon)
-
- override def run { main.run() }
-
- private var interruptible: Boolean = true
- private var interrupt_pending: Boolean = false
-
- override def interrupt: Unit = synchronized
- {
- if (interruptible) super.interrupt()
- else { interrupt_pending = true }
- }
-
- def uninterruptible[A](body: => A): A =
- {
- require(Thread.currentThread == thread)
-
- val interruptible0 = synchronized { val b = interruptible; interruptible = false; b }
- try { body }
- finally {
- synchronized {
- interruptible = interruptible0
- if (interruptible && interrupt_pending) {
- interrupt_pending = false
- super.interrupt()
- }
- }
- Exn.Interrupt.expose()
- }
- }
-}
--- a/src/Pure/Concurrent/timeout.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Concurrent/timeout.ML Sun Apr 05 13:05:40 2020 +0200
@@ -24,7 +24,7 @@
val request =
Event_Timer.request {physical = false} (start + timeout)
- (fn () => Standard_Thread.interrupt_unsynchronized self);
+ (fn () => Isabelle_Thread.interrupt_unsynchronized self);
val result =
Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
--- a/src/Pure/GUI/gui_thread.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/GUI/gui_thread.scala Sun Apr 05 13:05:40 2020 +0200
@@ -58,9 +58,9 @@
/* delayed events */
- def delay_first(delay: => Time)(event: => Unit): Standard_Thread.Delay =
- Standard_Thread.delay_first(delay) { later { event } }
+ def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_first(delay) { later { event } }
- def delay_last(delay: => Time)(event: => Unit): Standard_Thread.Delay =
- Standard_Thread.delay_last(delay) { later { event } }
+ def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(delay) { later { event } }
}
--- a/src/Pure/General/file_watcher.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/General/file_watcher.scala Sun Apr 05 13:05:40 2020 +0200
@@ -84,13 +84,13 @@
/* changed directory entries */
- private val delay_changed = Standard_Thread.delay_last(delay)
+ private val delay_changed = Isabelle_Thread.delay_last(delay)
{
val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty)))
handle(changed)
}
- private val watcher_thread = Standard_Thread.fork(name = "file_watcher", daemon = true)
+ private val watcher_thread = Isabelle_Thread.fork(name = "file_watcher", daemon = true)
{
try {
while (true) {
--- a/src/Pure/PIDE/headless.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/headless.scala Sun Apr 05 13:05:40 2020 +0200
@@ -304,12 +304,12 @@
val consumer =
{
val delay_nodes_status =
- Standard_Thread.delay_first(nodes_status_delay max Time.zero) {
+ Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) {
progress.nodes_status(use_theories_state.value.nodes_status)
}
val delay_commit_clean =
- Standard_Thread.delay_first(commit_cleanup_delay max Time.zero) {
+ Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) {
val clean_theories = use_theories_state.change_result(_.clean_theories)
if (clean_theories.nonEmpty) {
progress.echo("Removing " + clean_theories.length + " theories ...")
--- a/src/Pure/PIDE/prover.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/prover.scala Sun Apr 05 13:05:40 2020 +0200
@@ -112,7 +112,7 @@
}
}
- private val process_manager = Standard_Thread.fork(name = "process_manager")
+ private val process_manager = Isabelle_Thread.fork(name = "process_manager")
{
val stdout = physical_output(false)
@@ -218,7 +218,7 @@
if (err) ("standard_error", process.stderr, Markup.STDERR)
else ("standard_output", process.stdout, Markup.STDOUT)
- Standard_Thread.fork(name = name) {
+ Isabelle_Thread.fork(name = name) {
try {
var result = new StringBuilder(100)
var finished = false
@@ -256,7 +256,7 @@
class Protocol_Error(msg: String) extends Exception(msg)
val name = "message_output"
- Standard_Thread.fork(name = name) {
+ Isabelle_Thread.fork(name = name) {
val default_buffer = new Array[Byte](65536)
var c = -1
--- a/src/Pure/PIDE/session.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/PIDE/session.scala Sun Apr 05 13:05:40 2020 +0200
@@ -268,7 +268,7 @@
nodes = Set.empty
commands = Set.empty
}
- private val delay_flush = Standard_Thread.delay_first(output_delay) { flush() }
+ private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() }
def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit =
synchronized {
@@ -313,7 +313,7 @@
private object consolidation
{
private val delay =
- Standard_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
+ Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) }
private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
private val state = Synchronized(init_state)
@@ -382,7 +382,7 @@
/* manager thread */
private val delay_prune =
- Standard_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
+ Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
private val manager: Consumer_Thread[Any] =
{
--- a/src/Pure/ROOT.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/ROOT.ML Sun Apr 05 13:05:40 2020 +0200
@@ -117,7 +117,7 @@
ML_file "ML/ml_statistics.ML";
ML_file "Concurrent/thread_data_virtual.ML";
-ML_file "Concurrent/standard_thread.ML";
+ML_file "Concurrent/isabelle_thread.ML";
ML_file "Concurrent/single_assignment.ML";
ML_file "Concurrent/par_exn.ML";
--- a/src/Pure/System/bash.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/bash.ML Sun Apr 05 13:05:40 2020 +0200
@@ -38,7 +38,7 @@
val _ = cleanup_files ();
val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
@@ -86,7 +86,7 @@
in () end;
fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
+ (Isabelle_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
in
let
@@ -132,7 +132,7 @@
val _ = cleanup_files ();
val system_thread =
- Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
+ Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
@@ -182,7 +182,7 @@
in () end;
fun cleanup () =
- (Standard_Thread.interrupt_unsynchronized system_thread;
+ (Isabelle_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
in
let
--- a/src/Pure/System/command_line.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/command_line.scala Sun Apr 05 13:05:40 2020 +0200
@@ -26,7 +26,7 @@
def tool(body: => Unit)
{
val thread =
- Standard_Thread.fork(name = "command_line", inherit_locals = true) {
+ Isabelle_Thread.fork(name = "command_line", inherit_locals = true) {
val rc =
try { body; 0 }
catch {
--- a/src/Pure/System/message_channel.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/System/message_channel.ML Sun Apr 05 13:05:40 2020 +0200
@@ -59,11 +59,11 @@
let
val mbox = Mailbox.create ();
val thread =
- Standard_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
+ Isabelle_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
(message_output mbox stream);
fun send msg = Mailbox.send mbox (SOME msg);
fun shutdown () =
- (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Standard_Thread.join thread);
+ (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Isabelle_Thread.join thread);
in Message_Channel {send = send, shutdown = shutdown} end;
end;
--- a/src/Pure/Tools/debugger.ML Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/debugger.ML Sun Apr 05 13:05:40 2020 +0200
@@ -22,7 +22,7 @@
if msg = "" then ()
else
Output.protocol_message
- (Markup.debugger_output (Standard_Thread.the_name ()))
+ (Markup.debugger_output (Isabelle_Thread.the_name ()))
[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)];
val writeln_message = output_message Markup.writelnN;
@@ -250,7 +250,7 @@
(SOME (fn (_, break) =>
if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
then
- (case Standard_Thread.get_name () of
+ (case Isabelle_Thread.get_name () of
SOME thread_name => debugger_loop thread_name
| NONE => ())
else ()))));
--- a/src/Pure/Tools/debugger.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/debugger.scala Sun Apr 05 13:05:40 2020 +0200
@@ -155,7 +155,7 @@
private val state = Synchronized(Debugger.State())
private val delay_update =
- Standard_Thread.delay_first(session.output_delay) {
+ Isabelle_Thread.delay_first(session.output_delay) {
session.debugger_updates.post(Debugger.Update)
}
--- a/src/Pure/Tools/server.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/Tools/server.scala Sun Apr 05 13:05:40 2020 +0200
@@ -292,7 +292,7 @@
val progress: Connection_Progress = context.progress(ident)
def cancel { progress.stop }
- private lazy val thread = Standard_Thread.fork(name = "server_task")
+ private lazy val thread = Isabelle_Thread.fork(name = "server_task")
{
Exn.capture { body(task) } match {
case Exn.Res(res) =>
@@ -601,12 +601,12 @@
}
private lazy val server_thread: Thread =
- Standard_Thread.fork(name = "server") {
+ Isabelle_Thread.fork(name = "server") {
var finished = false
while (!finished) {
Exn.capture(server_socket.accept) match {
case Exn.Res(socket) =>
- Standard_Thread.fork(name = "server_connection")
+ Isabelle_Thread.fork(name = "server_connection")
{ using(Server.Connection(socket))(handle) }
case Exn.Exn(_) => finished = true
}
--- a/src/Pure/build-jars Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Pure/build-jars Sun Apr 05 13:05:40 2020 +0200
@@ -30,9 +30,9 @@
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
+ src/Pure/Concurrent/isabelle_thread.scala
src/Pure/Concurrent/mailbox.scala
src/Pure/Concurrent/par_list.scala
- src/Pure/Concurrent/standard_thread.scala
src/Pure/Concurrent/synchronized.scala
src/Pure/GUI/color_value.scala
src/Pure/GUI/gui.scala
--- a/src/Tools/Haskell/Haskell.thy Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/Haskell/Haskell.thy Sun Apr 05 13:05:40 2020 +0200
@@ -1715,20 +1715,20 @@
Just n -> fmap trim_line . fst <$> read_block socket n
\<close>
-generate_file "Isabelle/Standard_Thread.hs" = \<open>
-{- Title: Isabelle/Standard_Thread.hs
+generate_file "Isabelle/Isabelle_Thread.hs" = \<open>
+{- Title: Isabelle/Isabelle_Thread.hs
Author: Makarius
LICENSE: BSD 3-clause (Isabelle)
-Standard thread operations.
-
-See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.ML\<close>
-and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/standard_thread.scala\<close>.
+Isabelle-specific thread management.
+
+See \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.ML\<close>
+and \<^file>\<open>$ISABELLE_HOME/src/Pure/Concurrent/isabelle_thread.scala\<close>.
-}
{-# LANGUAGE NamedFieldPuns #-}
-module Isabelle.Standard_Thread (
+module Isabelle.Isabelle_Thread (
ThreadId, Result,
find_id,
properties, change_properties,
@@ -1912,7 +1912,7 @@
import Isabelle.Library
import qualified Isabelle.UUID as UUID
import qualified Isabelle.Byte_Message as Byte_Message
-import qualified Isabelle.Standard_Thread as Standard_Thread
+import qualified Isabelle.Isabelle_Thread as Isabelle_Thread
{- server address -}
@@ -1953,7 +1953,7 @@
loop :: Socket -> ByteString -> IO ()
loop server_socket password = forever $ do
(connection, _) <- Socket.accept server_socket
- Standard_Thread.fork_finally
+ Isabelle_Thread.fork_finally
(do
line <- Byte_Message.read_line connection
when (line == Just password) $ handle connection)
--- a/src/Tools/VSCode/src/server.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/VSCode/src/server.scala Sun Apr 05 13:05:40 2020 +0200
@@ -127,12 +127,12 @@
/* input from client or file-system */
- private val delay_input: Standard_Thread.Delay =
- Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_input: Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ resources.flush_input(session, channel) }
- private val delay_load: Standard_Thread.Delay =
- Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
+ private val delay_load: Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
val (invoke_input, invoke_load) =
resources.resolve_dependencies(session, editor, file_watcher)
if (invoke_input) delay_input.invoke()
@@ -183,8 +183,8 @@
/* caret handling */
- private val delay_caret_update: Standard_Thread.Delay =
- Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+ private val delay_caret_update: Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
{ session.caret_focus.post(Session.Caret_Focus) }
private def update_caret(caret: Option[(JFile, Line.Position)])
@@ -199,8 +199,8 @@
private lazy val preview_panel = new Preview_Panel(resources)
- private lazy val delay_preview: Standard_Thread.Delay =
- Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private lazy val delay_preview: Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (preview_panel.flush(channel)) delay_preview.invoke()
}
@@ -214,8 +214,8 @@
/* output to client */
- private val delay_output: Standard_Thread.Delay =
- Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
+ private val delay_output: Isabelle_Thread.Delay =
+ Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
{
if (resources.flush_output(channel)) delay_output.invoke()
}
--- a/src/Tools/jEdit/src/active.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/active.scala Sun Apr 05 13:05:40 2020 +0200
@@ -31,14 +31,14 @@
// FIXME avoid hard-wired stuff
elem match {
case XML.Elem(Markup(Markup.BROWSER, _), body) =>
- Standard_Thread.fork(name = "browser") {
+ Isabelle_Thread.fork(name = "browser") {
val graph_file = Isabelle_System.tmp_file("graph")
File.write(graph_file, XML.content(body))
Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
}
case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
- Standard_Thread.fork(name = "graphview") {
+ Isabelle_Thread.fork(name = "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/jedit_editor.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Apr 05 13:05:40 2020 +0200
@@ -181,7 +181,7 @@
if (path.is_file)
goto_file(true, view, File.platform_path(path))
else {
- Standard_Thread.fork(name = "documentation") {
+ Isabelle_Thread.fork(name = "documentation") {
try { Doc.view(path) }
catch {
case exn: Throwable =>
@@ -211,7 +211,7 @@
new Hyperlink {
override val external = true
def follow(view: View): Unit =
- Standard_Thread.fork(name = "hyperlink_url") {
+ Isabelle_Thread.fork(name = "hyperlink_url") {
try { Isabelle_System.open(Url.escape_name(name)) }
catch {
case exn: Throwable =>
--- a/src/Tools/jEdit/src/plugin.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sun Apr 05 13:05:40 2020 +0200
@@ -154,7 +154,7 @@
}
if (required_files.nonEmpty) {
try {
- Standard_Thread.fork(name = "resolve_dependencies") {
+ Isabelle_Thread.fork(name = "resolve_dependencies") {
val loaded_files =
for {
name <- required_files
--- a/src/Tools/jEdit/src/session_build.scala Sat Apr 04 21:38:20 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Sun Apr 05 13:05:40 2020 +0200
@@ -165,7 +165,7 @@
setLocationRelativeTo(view)
setVisible(true)
- Standard_Thread.fork(name = "session_build") {
+ Isabelle_Thread.fork(name = "session_build") {
progress.echo("Build started for Isabelle/" + PIDE.resources.session_name + " ...")
val (out, rc) =