# HG changeset patch
# User wenzelm
# Date 1459955790 -7200
# Node ID 7a11ea5c96266232f52453d541f03c72b8f471fd
# Parent  728aa05e943369669a610ce1a41de9a3d836250c
tuned signature;

diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/event_timer.ML
--- 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));
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/lazy.ML
--- 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
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/multithreading.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/par_list.ML
--- 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
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/single_assignment.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/synchronized.ML
--- 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);
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/task_queue.ML
--- 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) ();
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/thread_data.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Concurrent/unsynchronized.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/ML/exn_debugger.ML
--- 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) ();
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/ML/exn_properties.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/PIDE/execution.ML
--- 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 ();
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/PIDE/query_operation.ML
--- 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);
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/System/bash.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/System/command_line.ML
--- 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 =>
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/System/isabelle_process.ML
--- 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);
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/System/windows/bash.ML
--- 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;
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Thy/thy_info.ML
--- 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) =>
diff -r 728aa05e9433 -r 7a11ea5c9626 src/Pure/Tools/debugger.ML
--- 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 ());