--- a/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 14:28:55 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML Wed Aug 10 15:17:24 2011 +0200
@@ -144,7 +144,7 @@
NONE
else
let
- val _ = List.app (Simple_Thread.interrupt o #1) canceling
+ val _ = List.app (Simple_Thread.interrupt_unsynchronized o #1) canceling
val canceling' = filter (Thread.isActive o #1) canceling
val state' = make_state manager timeout_heap' active canceling' messages store;
in SOME (map #2 timeout_threads, state') end
--- a/src/Pure/Concurrent/bash.ML Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/bash.ML Wed Aug 10 15:17:24 2011 +0200
@@ -73,7 +73,7 @@
in () end;
fun cleanup () =
- (Simple_Thread.interrupt system_thread;
+ (Simple_Thread.interrupt_unsynchronized system_thread;
try File.rm script_path;
try File.rm output_path;
try File.rm pid_path);
--- a/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML Wed Aug 10 15:17:24 2011 +0200
@@ -8,7 +8,7 @@
sig
val attributes: bool -> Thread.threadAttribute list
val fork: bool -> (unit -> unit) -> Thread.thread
- val interrupt: Thread.thread -> unit
+ val interrupt_unsynchronized: Thread.thread -> unit
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
end;
@@ -24,7 +24,7 @@
body () handle exn => if Exn.is_interrupt exn then () else reraise exn),
attributes interrupts);
-fun interrupt thread = Thread.interrupt thread handle Thread _ => ();
+fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
(* basic synchronization *)
--- a/src/Pure/Concurrent/task_queue.ML Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Aug 10 15:17:24 2011 +0200
@@ -247,7 +247,7 @@
val running =
Tasks.fold (#1 #> get_job jobs #> (fn Running t => insert Thread.equal t | _ => I))
(get_tasks groups (group_id group)) [];
- val _ = List.app Simple_Thread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt_unsynchronized running;
in null running end;
fun cancel_all (Queue {jobs, ...}) =
@@ -262,7 +262,7 @@
| _ => (groups, running))
end;
val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
- val _ = List.app Simple_Thread.interrupt running;
+ val _ = List.app Simple_Thread.interrupt_unsynchronized running;
in running_groups end;
--- a/src/Pure/Concurrent/time_limit.ML Wed Aug 10 14:28:55 2011 +0200
+++ b/src/Pure/Concurrent/time_limit.ML Wed Aug 10 15:17:24 2011 +0200
@@ -30,12 +30,12 @@
val main = Thread.self ();
val timeout = Unsynchronized.ref false;
val watchdog = Simple_Thread.fork true (fn () =>
- (OS.Process.sleep time; timeout := true; Thread.interrupt main));
+ (OS.Process.sleep time; timeout := true; Simple_Thread.interrupt_unsynchronized main));
val result =
Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
- val _ = Thread.interrupt watchdog handle Thread _ => ();
+ val _ = Simple_Thread.interrupt_unsynchronized watchdog;
val _ = while Thread.isActive watchdog do OS.Process.sleep wait_time;
val test = Exn.capture Multithreading.interrupted ();