--- a/Admin/polyml/future/ROOT.ML Tue Nov 03 11:24:42 2015 +0100
+++ b/Admin/polyml/future/ROOT.ML Tue Nov 03 13:54:34 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/Tools/Sledgehammer/async_manager_legacy.ML Tue Nov 03 11:24:42 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/bash_windows.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/future.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/future.scala Tue Nov 03 13:54:34 2015 +0100
@@ -18,7 +18,7 @@
object Future
{
lazy val execution_context: ExecutionContextExecutor =
- ExecutionContext.fromExecutorService(Simple_Thread.default_pool)
+ ExecutionContext.fromExecutorService(Standard_Thread.default_pool)
def value[A](x: A): Future[A] = new Finished_Future(x)
--- a/src/Pure/Concurrent/par_list.scala Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/par_list.scala Tue Nov 03 13:54:34 2015 +0100
@@ -30,7 +30,7 @@
try {
state.change(_ =>
(xs.iterator.zipWithIndex.map({ case (x, self) =>
- Simple_Thread.submit_task {
+ Standard_Thread.submit_task {
val result = Exn.capture { f(x) }
result match { case Exn.Exn(_) => cancel_other(self) case _ => }
result
--- a/src/Pure/Concurrent/simple_thread.ML Tue Nov 03 11:24:42 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 11:24:42 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 => 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)
-}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/standard_thread.ML Tue Nov 03 13:54:34 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 13:54:34 2015 +0100
@@ -0,0 +1,110 @@
+/* Title: Pure/Concurrent/standard_thread.scala
+ Module: PIDE
+ Author: Makarius
+
+Standard thread operations.
+*/
+
+package isabelle
+
+
+import java.lang.Thread
+import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
+ TimeUnit, LinkedBlockingQueue}
+
+
+object Standard_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 [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 11:24:42 2015 +0100
+++ b/src/Pure/Concurrent/time_limit.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/GUI/gui_thread.scala Tue Nov 03 13:54:34 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/PIDE/prover.scala Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/PIDE/prover.scala Tue Nov 03 13:54:34 2015 +0100
@@ -122,7 +122,7 @@
/** process manager **/
private val (_, process_result) =
- Simple_Thread.future("process_result") { system_process.join }
+ Standard_Thread.future("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 11:24:42 2015 +0100
+++ b/src/Pure/PIDE/session.scala Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/ROOT Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/ROOT.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/System/invoke_scala.scala Tue Nov 03 13:54:34 2015 +0100
@@ -94,7 +94,7 @@
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
futures += (id ->
- Simple_Thread.submit_task {
+ Standard_Thread.submit_task {
val (tag, result) = Invoke_Scala.method(name, msg.text)
fulfill(prover, id, tag, result)
})
--- a/src/Pure/System/isabelle_system.scala Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Nov 03 13:54:34 2015 +0100
@@ -329,11 +329,11 @@
val limited = new Limited_Progress(proc, progress_limit)
val (_, stdout) =
- Simple_Thread.future("bash_stdout") {
+ Standard_Thread.future("bash_stdout") {
File.read_lines(proc.stdout, limited(progress_stdout))
}
val (_, stderr) =
- Simple_Thread.future("bash_stderr") {
+ Standard_Thread.future("bash_stderr") {
File.read_lines(proc.stderr, limited(progress_stderr))
}
--- a/src/Pure/System/message_channel.ML Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/System/message_channel.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 03 13:54:34 2015 +0100
@@ -599,7 +599,7 @@
}
private val (thread, result) =
- Simple_Thread.future("build") {
+ Standard_Thread.future("build") {
Isabelle_System.bash_env(info.dir.file, env, script,
progress_stdout = (line: String) =>
Library.try_unprefix("\floading_theory = ", line) match {
--- a/src/Pure/Tools/debugger.ML Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Pure/Tools/debugger.ML Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/Tools/debugger.scala Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Pure/build-jars Tue Nov 03 13:54:34 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/pretty_text_area.scala Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Nov 03 13:54:34 2015 +0100
@@ -130,7 +130,7 @@
future_refresh.map(_.cancel(true))
future_refresh =
- Some(Simple_Thread.submit_task {
+ Some(Standard_Thread.submit_task {
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/session_build.scala Tue Nov 03 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Tue Nov 03 13:54:34 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 11:24:42 2015 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Tue Nov 03 13:54:34 2015 +0100
@@ -128,7 +128,7 @@
}
future_refresh =
- Some(Simple_Thread.submit_task {
+ Some(Standard_Thread.submit_task {
val line_count = overview.line_count
val char_count = overview.char_count
val L = overview.L