# HG changeset patch
# User wenzelm
# Date 1459954312 -7200
# Node ID 728aa05e943369669a610ce1a41de9a3d836250c
# Parent  99c7f31615c2b0978298d36d1522838706c1ba28
clarified bootstrap;

diff -r 99c7f31615c2 -r 728aa05e9433 src/Pure/Concurrent/thread_data.ML
--- a/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:33:33 2016 +0200
+++ b/src/Pure/Concurrent/thread_data.ML	Wed Apr 06 16:51:52 2016 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Concurrent/thread_data.ML
     Author:     Makarius
 
-Thread-local data -- raw version without context management.
+Thread-local data -- physical version without context management.
 *)
 
 signature THREAD_DATA =
@@ -11,11 +11,63 @@
   val get: 'a var -> 'a option
   val put: 'a var -> 'a option -> unit
   val setmp: 'a var -> 'a option -> ('b -> 'c) -> 'b -> 'c
+  val is_virtual: bool
 end;
 
 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 *)
+
+local
+
+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;
+
+in
+
+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
 
@@ -39,4 +91,6 @@
 
 end;
 
+val is_virtual = false;
+
 end;
diff -r 99c7f31615c2 -r 728aa05e9433 src/Pure/ML/ml_name_space.ML
--- a/src/Pure/ML/ml_name_space.ML	Wed Apr 06 16:33:33 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML	Wed Apr 06 16:51:52 2016 +0200
@@ -63,7 +63,7 @@
   val bootstrap_values =
     ["use", "exit", "ML_system_pretty", "ML_system_pp", "ML_system_overload"];
   val bootstrap_structures =
-    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
+    ["PolyML", "CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal", "Thread_Data"];
 
 
   (* Standard ML environment *)
diff -r 99c7f31615c2 -r 728aa05e9433 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Wed Apr 06 16:33:33 2016 +0200
+++ b/src/Pure/ROOT.ML	Wed Apr 06 16:51:52 2016 +0200
@@ -12,7 +12,6 @@
 use "General/exn.ML";
 
 use "Concurrent/multithreading.ML";
-use "Concurrent/thread_data.ML";
 use "Concurrent/unsynchronized.ML";
 
 use "ML/ml_heap.ML";
diff -r 99c7f31615c2 -r 728aa05e9433 src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Wed Apr 06 16:33:33 2016 +0200
+++ b/src/Pure/ROOT0.ML	Wed Apr 06 16:51:52 2016 +0200
@@ -1,2 +1,3 @@
 (*** Isabelle/Pure bootstrap: initial setup ***)
 
+use "Concurrent/thread_data.ML";