--- a/src/Pure/Concurrent/event_timer.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.ML Wed Apr 06 17:16:30 2016 +0200
@@ -109,7 +109,7 @@
manager_loop);
fun shutdown () =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
if Synchronized.change_result state (fn st as State {requests, manager, ...} =>
if is_shutdown Normal st then (false, st)
else if is_shutdown Shutdown_Ack st orelse is_shutdown_req st then
@@ -144,7 +144,7 @@
val manager' = manager_check manager;
in (canceled, make_state (requests', status, manager')) end);
-val future = uninterruptible (fn _ => fn time =>
+val future = Multithreading.uninterruptible (fn _ => fn time =>
let
val req: request Single_Assignment.var = Single_Assignment.var "request";
fun abort () = ignore (cancel (Single_Assignment.await req));
--- a/src/Pure/Concurrent/lazy.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML Wed Apr 06 17:16:30 2016 +0200
@@ -61,7 +61,7 @@
(case peek (Lazy var) of
SOME res => res
| NONE =>
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val (expr, x) =
Synchronized.change_result var
--- a/src/Pure/Concurrent/multithreading.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML Wed Apr 06 17:16:30 2016 +0200
@@ -4,21 +4,16 @@
Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
*)
-signature BASIC_MULTITHREADING =
-sig
- val interruptible: ('a -> 'b) -> 'a -> 'b
- val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
signature MULTITHREADING =
sig
- include BASIC_MULTITHREADING
val no_interrupts: Thread.threadAttribute list
val public_interrupts: Thread.threadAttribute list
val private_interrupts: Thread.threadAttribute list
val sync_interrupts: Thread.threadAttribute list -> Thread.threadAttribute list
val interrupted: unit -> unit (*exception Interrupt*)
val with_attributes: Thread.threadAttribute list -> (Thread.threadAttribute list -> 'a) -> 'a
+ val interruptible: ('a -> 'b) -> 'a -> 'b
+ val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
val max_threads_value: unit -> int
val max_threads_update: int -> unit
val enabled: unit -> bool
@@ -75,9 +70,6 @@
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
-
-(* portable wrappers *)
-
fun interruptible f x = with_attributes public_interrupts (fn _ => f x);
fun uninterruptible f x =
@@ -179,6 +171,3 @@
end;
end;
-
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;
--- a/src/Pure/Concurrent/par_list.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/par_list.ML Wed Apr 06 17:16:30 2016 +0200
@@ -33,7 +33,7 @@
if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
then map (Exn.capture f) xs
else
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val (group, pri) =
(case Future.worker_task () of
--- a/src/Pure/Concurrent/single_assignment.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML Wed Apr 06 17:16:30 2016 +0200
@@ -48,7 +48,7 @@
(case peek v of
SOME _ => raise Fail ("Duplicate assignment to " ^ name)
| NONE =>
- uninterruptible (fn _ => fn () =>
+ Multithreading.uninterruptible (fn _ => fn () =>
(SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
end;
--- a/src/Pure/Concurrent/synchronized.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Wed Apr 06 17:16:30 2016 +0200
@@ -51,7 +51,7 @@
| Exn.Res false => NONE
| Exn.Exn exn => Exn.reraise exn)
| SOME (y, x') =>
- uninterruptible (fn _ => fn () =>
+ Multithreading.uninterruptible (fn _ => fn () =>
(var := x'; ConditionVar.broadcast cond; SOME y)) ())
end;
in try_change () end);
--- a/src/Pure/Concurrent/task_queue.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Wed Apr 06 17:16:30 2016 +0200
@@ -135,7 +135,7 @@
fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
fun update_timing update (Task {timing, ...}) e =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val start = Time.now ();
val result = Exn.capture (restore_attributes e) ();
--- a/src/Pure/Concurrent/thread_data.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/thread_data.ML Wed Apr 06 17:16:30 2016 +0200
@@ -39,7 +39,8 @@
(* thread attributes *)
-local
+structure Multithreading =
+struct
val no_interrupts =
[Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
@@ -57,8 +58,6 @@
val _ = Thread.setAttributes orig_atts;
in Exn.release result end;
-in
-
fun uninterruptible f x =
with_attributes no_interrupts (fn atts =>
f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
@@ -81,7 +80,7 @@
fun put (Var tag) data = Thread.setLocal (tag, data);
fun setmp v data f x =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val orig_data = get v;
val _ = put v data;
--- a/src/Pure/Concurrent/unsynchronized.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML Wed Apr 06 17:16:30 2016 +0200
@@ -19,7 +19,7 @@
fun dec i = (i := ! i - (1: int); ! i);
fun setmp flag value f x =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val orig_value = ! flag;
val _ = flag := value;
--- a/src/Pure/ML/exn_debugger.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML Wed Apr 06 17:16:30 2016 +0200
@@ -42,7 +42,7 @@
in
fun capture_exception_trace e =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val _ = start_trace ();
val result = Exn.interruptible_capture (restore_attributes e) ();
--- a/src/Pure/ML/exn_properties.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/ML/exn_properties.ML Wed Apr 06 17:16:30 2016 +0200
@@ -63,7 +63,7 @@
startLine = #startLine loc, endLine = #endLine loc,
startPosition = #startPosition loc, endPosition = #endPosition loc};
in
- uninterruptible (fn _ => fn () =>
+ Multithreading.uninterruptible (fn _ => fn () =>
PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
end
end;
--- a/src/Pure/PIDE/execution.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/PIDE/execution.ML Wed Apr 06 17:16:30 2016 +0200
@@ -89,7 +89,7 @@
type params = {name: string, pos: Position.T, pri: int};
fun fork ({name, pos, pri}: params) e =
- uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
+ Multithreading.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
let
val exec_id = the_default 0 (Position.parse_id pos);
val group = Future.worker_subgroup ();
--- a/src/Pure/PIDE/query_operation.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/PIDE/query_operation.ML Wed Apr 06 17:16:30 2016 +0200
@@ -19,7 +19,7 @@
Command.print_function (name ^ "_query")
(fn {args = instance :: args, ...} =>
SOME {delay = NONE, pri = pri, persistent = false, strict = false,
- print_fn = fn _ => uninterruptible (fn restore_attributes => fn state =>
+ print_fn = fn _ => Multithreading.uninterruptible (fn restore_attributes => fn state =>
let
fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
fun status m = output_result (Markup.markup_only m);
--- a/src/Pure/System/bash.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/System/bash.ML Wed Apr 06 17:16:30 2016 +0200
@@ -12,7 +12,7 @@
structure Bash: BASH =
struct
-val process = uninterruptible (fn restore_attributes => fn script =>
+val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
--- a/src/Pure/System/command_line.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/System/command_line.ML Wed Apr 06 17:16:30 2016 +0200
@@ -14,7 +14,7 @@
struct
fun tool body =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
val rc =
restore_attributes body () handle exn =>
--- a/src/Pure/System/isabelle_process.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Apr 06 17:16:30 2016 +0200
@@ -187,7 +187,7 @@
val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
val default_modes2 = [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN];
-val init_protocol = uninterruptible (fn _ => fn socket =>
+val init_protocol = Multithreading.uninterruptible (fn _ => fn socket =>
let
val _ = SHA1.test_samples ()
handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
--- a/src/Pure/System/windows/bash.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/System/windows/bash.ML Wed Apr 06 17:16:30 2016 +0200
@@ -12,7 +12,7 @@
structure Bash: BASH =
struct
-val process = uninterruptible (fn restore_attributes => fn script =>
+val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
--- a/src/Pure/Thy/thy_info.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Apr 06 17:16:30 2016 +0200
@@ -185,7 +185,7 @@
in result_theory result end
| Finished thy => thy)) #> ignore;
-val schedule_futures = uninterruptible (fn _ => fn tasks =>
+val schedule_futures = Multithreading.uninterruptible (fn _ => fn tasks =>
let
val futures = tasks
|> String_Graph.schedule (fn deps => fn (name, task) =>
--- a/src/Pure/Tools/debugger.ML Wed Apr 06 16:51:52 2016 +0200
+++ b/src/Pure/Tools/debugger.ML Wed Apr 06 17:16:30 2016 +0200
@@ -227,7 +227,7 @@
in
fun debugger_loop thread_name =
- uninterruptible (fn restore_attributes => fn () =>
+ Multithreading.uninterruptible (fn restore_attributes => fn () =>
let
fun loop () =
(debugger_state thread_name; if debugger_command thread_name then loop () else ());