# HG changeset patch
# User wenzelm
# Date 1460203223 -7200
# Node ID 3a122e1e352a1100edf0889a133ceb0368106e3a
# Parent  96691631c1ebaa1a25d9ef8e44791ba6447dcd16
clarified bootstrap;

diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/event_timer.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -109,7 +109,7 @@
       manager_loop);
 
 fun shutdown () =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.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 = Multithreading.uninterruptible (fn _ => fn time =>
+val future = Thread_Attributes.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 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/future.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -206,10 +206,10 @@
   broadcast scheduler_event);
 
 fun interruptible_task f x =
-  Multithreading.with_attributes
+  Thread_Attributes.with_attributes
     (if is_some (worker_task ())
-     then Multithreading.private_interrupts
-     else Multithreading.public_interrupts)
+     then Thread_Attributes.private_interrupts
+     else Thread_Attributes.public_interrupts)
     (fn _ => f x)
   before Multithreading.interrupted ();
 
@@ -359,8 +359,8 @@
 
 fun scheduler_loop () =
  (while
-    Multithreading.with_attributes
-      (Multithreading.sync_interrupts Multithreading.public_interrupts)
+    Thread_Attributes.with_attributes
+      (Thread_Attributes.sync_interrupts Thread_Attributes.public_interrupts)
       (fn _ => SYNCHRONIZED "scheduler" (fn () => scheduler_next ()))
   do (); last_round := Time.zeroTime);
 
@@ -438,7 +438,7 @@
         val res =
           if ok then
             Exn.capture (fn () =>
-              Multithreading.with_attributes atts (fn _ =>
+              Thread_Attributes.with_attributes atts (fn _ =>
                 (Position.setmp_thread_data pos o Context.setmp_generic_context context) e ())) ()
           else Exn.interrupt_exn;
       in assign_result group result (identify_result pos res) end;
@@ -462,8 +462,8 @@
         let
           val atts =
             if interrupts
-            then Multithreading.private_interrupts
-            else Multithreading.no_interrupts;
+            then Thread_Attributes.private_interrupts
+            else Thread_Attributes.no_interrupts;
           val (result, job) = future_job grp atts e;
           val (task, queue') = Task_Queue.enqueue name grp deps pri job queue;
           val future = Future {promised = false, task = task, result = result};
@@ -504,7 +504,7 @@
       (NONE, []) => NONE
     | (NONE, deps') =>
        (worker_waiting deps' (fn () =>
-          Multithreading.with_attributes atts (fn _ =>
+          Thread_Attributes.with_attributes atts (fn _ =>
             Exn.release (worker_wait Waiting work_finished)));
         join_next atts deps')
     | (SOME work, deps') => SOME (work, deps'));
@@ -521,7 +521,7 @@
     val _ =
       if forall is_finished xs then ()
       else if is_some (worker_task ()) then
-        Multithreading.with_attributes Multithreading.no_interrupts
+        Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
           (fn orig_atts => join_loop orig_atts (map task_of xs))
       else List.app (ignore o Single_Assignment.await o result_of) xs;
   in map get_result xs end;
@@ -544,7 +544,7 @@
 (* task context for running thread *)
 
 fun task_context name group f x =
-  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+  Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
     let
       val (result, job) = future_job group orig_atts (fn () => f x);
       val task =
@@ -581,7 +581,7 @@
       val task = task_of x;
       val group = Task_Queue.group_of_task task;
       val (result, job) =
-        future_job group Multithreading.private_interrupts (fn () => f (join x));
+        future_job group Thread_Attributes.private_interrupts (fn () => f (join x));
 
       val extended = SYNCHRONIZED "extend" (fn () =>
         (case Task_Queue.extend task job (! queue) of
@@ -609,7 +609,7 @@
             then raise Fail "Concurrent attempt to fulfill promise"
             else Exn.reraise exn;
     fun job () =
-      Multithreading.with_attributes Multithreading.no_interrupts
+      Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
         (fn _ => Exn.release (Exn.capture assign () before abort ()));
     val task = SYNCHRONIZED "enqueue_passive" (fn () =>
       Unsynchronized.change_result queue (Task_Queue.enqueue_passive group job));
@@ -626,7 +626,7 @@
       fun job ok =
         assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
       val _ =
-        Multithreading.with_attributes Multithreading.no_interrupts (fn _ =>
+        Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
           let
             val passive_job =
               SYNCHRONIZED "fulfill_result" (fn () =>
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -61,7 +61,7 @@
   (case peek (Lazy var) of
     SOME res => res
   | NONE =>
-      Multithreading.uninterruptible (fn restore_attributes => fn () =>
+      Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
         let
           val (expr, x) =
             Synchronized.change_result var
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/multithreading.ML
--- a/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/multithreading.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -6,13 +6,7 @@
 
 signature MULTITHREADING =
 sig
-  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 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
@@ -28,50 +22,16 @@
 structure Multithreading: MULTITHREADING =
 struct
 
-(* thread attributes *)
-
-val no_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val test_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptSynch];
-
-val public_interrupts =
-  [Thread.EnableBroadcastInterrupt true, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val private_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptAsynchOnce];
-
-val sync_interrupts = map
-  (fn x as Thread.InterruptState Thread.InterruptDefer => x
-    | Thread.InterruptState _ => Thread.InterruptState Thread.InterruptSynch
-    | x => x);
-
-val safe_interrupts = map
-  (fn Thread.InterruptState Thread.InterruptAsynch =>
-      Thread.InterruptState Thread.InterruptAsynchOnce
-    | x => x);
+(* interrupts *)
 
 fun interrupted () =
   let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val _ = Thread.setAttributes test_interrupts;
+    val orig_atts = Thread_Attributes.safe_interrupts (Thread.getAttributes ());
+    val _ = Thread.setAttributes Thread_Attributes.test_interrupts;
     val test = Exn.capture Thread.testInterrupt ();
     val _ = Thread.setAttributes orig_atts;
   in Exn.release test end;
 
-fun with_attributes new_atts e =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val result = Exn.capture (fn () =>
-      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release result end;
-
-fun uninterruptible f x =
-  with_attributes no_interrupts (fn atts =>
-    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
 
 (* options *)
 
@@ -93,8 +53,9 @@
 (* synchronous wait *)
 
 fun sync_wait opt_atts time cond lock =
-  with_attributes
-    (sync_interrupts (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
+  Thread_Attributes.with_attributes
+    (Thread_Attributes.sync_interrupts
+      (case opt_atts of SOME atts => atts | NONE => Thread.getAttributes ()))
     (fn _ =>
       (case time of
         SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
@@ -108,7 +69,7 @@
 
 fun tracing level msg =
   if level > ! trace then ()
-  else uninterruptible (fn _ => fn () =>
+  else Thread_Attributes.uninterruptible (fn _ => fn () =>
     (TextIO.output (TextIO.stdErr, (">>> " ^ msg () ^ "\n")); TextIO.flushOut TextIO.stdErr)
       handle _ (*sic*) => ()) ();
 
@@ -131,7 +92,7 @@
 (* synchronized evaluation *)
 
 fun synchronized name lock e =
-  Exn.release (uninterruptible (fn restore_attributes => fn () =>
+  Exn.release (Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val immediate =
         if Mutex.trylock lock then true
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/par_list.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -33,7 +33,7 @@
   if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
   then map (Exn.capture f) xs
   else
-    Multithreading.uninterruptible (fn restore_attributes => fn () =>
+    Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
       let
         val (group, pri) =
           (case Future.worker_task () of
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -48,7 +48,7 @@
     (case peek v of
       SOME _ => raise Fail ("Duplicate assignment to " ^ name)
     | NONE =>
-        Multithreading.uninterruptible (fn _ => fn () =>
+        Thread_Attributes.uninterruptible (fn _ => fn () =>
          (SingleAssignment.saset (var, x); ConditionVar.broadcast cond)) ()));
 
 end;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/standard_thread.ML
--- a/src/Pure/Concurrent/standard_thread.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/standard_thread.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -50,7 +50,7 @@
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
   Thread.MaximumMLStack stack_limit ::
-  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+  (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
 
 fun fork (params: params) body =
   Thread.fork (fn () =>
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -51,7 +51,7 @@
               | Exn.Res false => NONE
               | Exn.Exn exn => Exn.reraise exn)
           | SOME (y, x') =>
-              Multithreading.uninterruptible (fn _ => fn () =>
+              Thread_Attributes.uninterruptible (fn _ => fn () =>
                 (var := x'; ConditionVar.broadcast cond; SOME y)) ())
         end;
     in try_change () end);
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 09 14:00:23 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 =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val start = Time.now ();
       val result = Exn.capture (restore_attributes e) ();
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/thread_attributes.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/thread_attributes.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -0,0 +1,63 @@
+(*  Title:      Pure/Concurrent/thread_attributes.ML
+    Author:     Makarius
+
+Thread attributes for interrupt handling.
+*)
+
+signature THREAD_ATTRIBUTES =
+sig
+  type attributes = Thread.Thread.threadAttribute list
+  val no_interrupts: attributes
+  val test_interrupts: attributes
+  val public_interrupts: attributes
+  val private_interrupts: attributes
+  val sync_interrupts: attributes -> attributes
+  val safe_interrupts: attributes -> attributes
+  val with_attributes: attributes -> (attributes -> 'a) -> 'a
+  val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
+end;
+
+structure Thread_Attributes: THREAD_ATTRIBUTES =
+struct
+
+type attributes = Thread.Thread.threadAttribute list;
+
+val no_interrupts =
+  [Thread.Thread.EnableBroadcastInterrupt false,
+    Thread.Thread.InterruptState Thread.Thread.InterruptDefer];
+
+val test_interrupts =
+  [Thread.Thread.EnableBroadcastInterrupt false,
+    Thread.Thread.InterruptState Thread.Thread.InterruptSynch];
+
+val public_interrupts =
+  [Thread.Thread.EnableBroadcastInterrupt true,
+    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+
+val private_interrupts =
+  [Thread.Thread.EnableBroadcastInterrupt false,
+    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+
+val sync_interrupts = map
+  (fn x as Thread.Thread.InterruptState Thread.Thread.InterruptDefer => x
+    | Thread.Thread.InterruptState _ => Thread.Thread.InterruptState Thread.Thread.InterruptSynch
+    | x => x);
+
+val safe_interrupts = map
+  (fn Thread.Thread.InterruptState Thread.Thread.InterruptAsynch =>
+      Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce
+    | x => x);
+
+fun with_attributes new_atts e =
+  let
+    val orig_atts = safe_interrupts (Thread.Thread.getAttributes ());
+    val result = Exn.capture (fn () =>
+      (Thread.Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
+    val _ = Thread.Thread.setAttributes orig_atts;
+  in Exn.release result end;
+
+fun uninterruptible f x =
+  with_attributes no_interrupts (fn atts =>
+    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
+
+end;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/thread_data.ML
--- a/src/Pure/Concurrent/thread_data.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/thread_data.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -17,70 +17,20 @@
 structure Thread_Data: THREAD_DATA =
 struct
 
-open Thread;
-
-
-(* exceptions as values *)
-
-structure Exn =
-struct
-
-datatype 'a result =
-  Res of 'a |
-  Exn of exn;
-
-fun capture f x = Res (f x) handle e => Exn e;
-
-fun release (Res y) = y
-  | release (Exn e) = PolyML.Exception.reraise e;
-
-end;
-
-
-(* thread attributes *)
-
-structure Multithreading =
-struct
-
-val no_interrupts =
-  [Thread.EnableBroadcastInterrupt false, Thread.InterruptState Thread.InterruptDefer];
-
-val safe_interrupts = map
-  (fn Thread.InterruptState Thread.InterruptAsynch =>
-      Thread.InterruptState Thread.InterruptAsynchOnce
-    | x => x);
-
-fun with_attributes new_atts e =
-  let
-    val orig_atts = safe_interrupts (Thread.getAttributes ());
-    val result = Exn.capture (fn () =>
-      (Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
-    val _ = Thread.setAttributes orig_atts;
-  in Exn.release result end;
-
-fun uninterruptible f x =
-  with_attributes no_interrupts (fn atts =>
-    f (fn g => fn y => with_attributes atts (fn _ => g y)) x);
-
-end;
-
-
-(* var *)
-
 abstype 'a var = Var of 'a option Universal.tag
 with
 
 fun var () : 'a var = Var (Universal.tag ());
 
 fun get (Var tag) =
-  (case Thread.getLocal tag of
+  (case Thread.Thread.getLocal tag of
     SOME data => data
   | NONE => NONE);
 
-fun put (Var tag) data = Thread.setLocal (tag, data);
+fun put (Var tag) data = Thread.Thread.setLocal (tag, data);
 
 fun setmp v data f x =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val orig_data = get v;
       val _ = put v data;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/thread_data_virtual.ML
--- a/src/Pure/Concurrent/thread_data_virtual.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/thread_data_virtual.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -7,8 +7,6 @@
 structure Thread_Data_Virtual: THREAD_DATA =
 struct
 
-(* context data *)
-
 structure Data = Generic_Data
 (
   type T = Universal.universal Inttab.table;
@@ -33,7 +31,7 @@
     | SOME x => Inttab.update (i, Universal.tagInject tag x));
 
 fun setmp v data f x =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val orig_data = get v;
       val _ = put v data;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/timeout.ML
--- a/src/Pure/Concurrent/timeout.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/timeout.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -17,7 +17,7 @@
 exception TIMEOUT of Time.time;
 
 fun apply timeout f x =
-  Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts =>
+  Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
     let
       val self = Thread.self ();
       val start = Time.now ();
@@ -26,7 +26,7 @@
         Event_Timer.request (start + timeout)
           (fn () => Standard_Thread.interrupt_unsynchronized self);
       val result =
-        Exn.capture (fn () => Multithreading.with_attributes orig_atts (fn _ => f x)) ();
+        Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
 
       val stop = Time.now ();
       val was_timeout = not (Event_Timer.cancel request);
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Concurrent/unsynchronized.ML
--- a/src/Pure/Concurrent/unsynchronized.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Concurrent/unsynchronized.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -19,7 +19,7 @@
 fun dec i = (i := ! i - (1: int); ! i);
 
 fun setmp flag value f x =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val orig_value = ! flag;
       val _ = flag := value;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/General/exn.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -127,8 +127,3 @@
       in reraise exn end);
 
 end;
-
-datatype illegal = Interrupt;
-
-structure Basic_Exn: BASIC_EXN = Exn;
-open Basic_Exn;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ML/exn_debugger.ML
--- a/src/Pure/ML/exn_debugger.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/exn_debugger.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -42,7 +42,7 @@
 in
 
 fun capture_exception_trace e =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val _ = start_trace ();
       val result = Exn.interruptible_capture (restore_attributes e) ();
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ML/exn_properties.ML
--- a/src/Pure/ML/exn_properties.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/exn_properties.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -63,7 +63,7 @@
               startLine = #startLine loc, endLine = #endLine loc,
               startPosition = #startPosition loc, endPosition = #endPosition loc};
         in
-          Multithreading.uninterruptible (fn _ => fn () =>
+          Thread_Attributes.uninterruptible (fn _ => fn () =>
             PolyML.raiseWithLocation (exn, loc') handle exn' => exn') ()
         end
     end;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -63,11 +63,11 @@
   val bootstrap_values =
     ["use", "exit", "ML_file", "ML_system_pretty", "ML_system_pp", "ML_system_overload",
       "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
+  val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
   val bootstrap_structures =
-    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data",
-      "ML_Recursive"];
+    ["Exn", "Basic_Exn", "Thread_Data", "ML_Recursive", "PolyML"] @ hidden_structures;
   val bootstrap_signatures =
-    ["THREAD_DATA", "ML_RECURSIVE"];
+    ["EXN", "BASIC_EXN", "THREAD_DATA", "ML_RECURSIVE"];
 
 
   (* Standard ML environment *)
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ML/ml_pervasive0.ML
--- a/src/Pure/ML/ml_pervasive0.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_pervasive0.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -26,3 +26,8 @@
 val error_depth = PolyML.error_depth;
 
 open Thread;
+
+datatype illegal = Interrupt;
+
+structure Basic_Exn: BASIC_EXN = Exn;
+open Basic_Exn;
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ML/ml_pervasive1.ML
--- a/src/Pure/ML/ml_pervasive1.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ML/ml_pervasive1.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -4,8 +4,7 @@
 Pervasive ML environment: final setup.
 *)
 
-List.app ML_Name_Space.forget_structure
-  (remove (op =) "PolyML" ML_Name_Space.bootstrap_structures);
+List.app ML_Name_Space.forget_structure ML_Name_Space.hidden_structures;
 
 structure PolyML = struct structure IntInf = PolyML.IntInf end;
 
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/PIDE/execution.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -89,7 +89,7 @@
 type params = {name: string, pos: Position.T, pri: int};
 
 fun fork ({name, pos, pri}: params) e =
-  Multithreading.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () =>
+  Thread_Attributes.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 96691631c1eb -r 3a122e1e352a src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Sat Apr 09 14:00:23 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 _ => Multithreading.uninterruptible (fn restore_attributes => fn state =>
+        print_fn = fn _ => Thread_Attributes.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 96691631c1eb -r 3a122e1e352a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ROOT.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -9,7 +9,6 @@
 ML_file "ML/ml_system.ML";
 ML_file "System/distribution.ML";
 
-ML_file "General/exn.ML";
 ML_file "General/basics.ML";
 
 ML_file "Concurrent/multithreading.ML";
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/ROOT0.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -1,4 +1,8 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
+ML_file "General/exn.ML";
+
+ML_file "Concurrent/thread_attributes.ML";
 ML_file "Concurrent/thread_data.ML";
-ML_file "ML/ml_recursive.ML"
+
+ML_file "ML/ml_recursive.ML";
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/System/bash.ML
--- a/src/Pure/System/bash.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/bash.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -14,7 +14,7 @@
 structure Bash: BASH =
 struct
 
-val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
+val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -34,7 +34,7 @@
 
     val system_thread =
       Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
-        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
             val bash_script =
@@ -105,7 +105,7 @@
 structure Bash: BASH =
 struct
 
-val process = Multithreading.uninterruptible (fn restore_attributes => fn script =>
+val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
   let
     datatype result = Wait | Signal | Result of int;
     val result = Synchronized.var "bash_result" Wait;
@@ -125,7 +125,7 @@
 
     val system_thread =
       Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
-        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
+        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
             val _ = getenv_strict "ISABELLE_BASH_PROCESS";
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/System/command_line.ML
--- a/src/Pure/System/command_line.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/command_line.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -14,7 +14,7 @@
 struct
 
 fun tool body =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val rc =
         restore_attributes body () handle exn =>
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML	Sat Apr 09 14:00:23 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 = Multithreading.uninterruptible (fn _ => fn socket =>
+val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn socket =>
   let
     val _ = SHA1.test_samples ()
       handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn);
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -185,7 +185,7 @@
         in result_theory result end
     | Finished thy => thy)) #> ignore;
 
-val schedule_futures = Multithreading.uninterruptible (fn _ => fn tasks =>
+val schedule_futures = Thread_Attributes.uninterruptible (fn _ => fn tasks =>
   let
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
diff -r 96691631c1eb -r 3a122e1e352a src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Sat Apr 09 13:28:32 2016 +0200
+++ b/src/Pure/Tools/debugger.ML	Sat Apr 09 14:00:23 2016 +0200
@@ -227,7 +227,7 @@
 in
 
 fun debugger_loop thread_name =
-  Multithreading.uninterruptible (fn restore_attributes => fn () =>
+  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       fun loop () =
         (debugger_state thread_name; if debugger_command thread_name then loop () else ());