more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;

--- a/src/Pure/Concurrent/multithreading.ML	Tue Dec 13 11:51:42 2016 +0100
+++ b/src/Pure/Concurrent/multithreading.ML	Tue Dec 13 23:29:54 2016 +0100
@@ -48,7 +48,7 @@
 
 fun sync_wait time cond lock =
   Thread_Attributes.with_attributes
-    (Thread_Attributes.sync_interrupts (Thread.getAttributes ()))
+    (Thread_Attributes.sync_interrupts (Thread_Attributes.get_attributes ()))
     (fn _ =>
       (case time of
         SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))

--- a/src/Pure/Concurrent/standard_thread.ML	Tue Dec 13 11:51:42 2016 +0100
+++ b/src/Pure/Concurrent/standard_thread.ML	Tue Dec 13 23:29:54 2016 +0100
@@ -50,7 +50,8 @@
 
 fun attributes ({stack_limit, interrupts, ...}: params) =
   Thread.MaximumMLStack stack_limit ::
-  (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
+  Thread_Attributes.convert_attributes
+    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
 
 fun fork (params: params) body =
   Thread.fork (fn () =>

--- a/src/Pure/Concurrent/thread_attributes.ML	Tue Dec 13 11:51:42 2016 +0100
+++ b/src/Pure/Concurrent/thread_attributes.ML	Tue Dec 13 23:29:54 2016 +0100
@@ -6,7 +6,10 @@
 
 signature THREAD_ATTRIBUTES =
 sig
-  type attributes = Thread.Thread.threadAttribute list
+  type attributes
+  val get_attributes: unit -> attributes
+  val set_attributes: attributes -> unit
+  val convert_attributes: attributes -> Thread.Thread.threadAttribute list
   val no_interrupts: attributes
   val test_interrupts: attributes
   val public_interrupts: attributes
@@ -21,40 +24,77 @@
 structure Thread_Attributes: THREAD_ATTRIBUTES =
 struct
 
-type attributes = Thread.Thread.threadAttribute list;
+abstype attributes = Attributes of Word.word
+with
 
-val no_interrupts =
-  [Thread.Thread.EnableBroadcastInterrupt false,
-    Thread.Thread.InterruptState Thread.Thread.InterruptDefer];
+(* thread attributes *)
+
+val thread_attributes = 0w7;
+
+val broadcast = 0w1;
 
-val test_interrupts =
-  [Thread.Thread.EnableBroadcastInterrupt false,
-    Thread.Thread.InterruptState Thread.Thread.InterruptSynch];
+val interrupt_state = 0w6;
+val interrupt_defer = 0w0;
+val interrupt_synch = 0w2;
+val interrupt_asynch = 0w4;
+val interrupt_asynch_once = 0w6;
+
 
-val public_interrupts =
-  [Thread.Thread.EnableBroadcastInterrupt true,
-    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+(* access thread flags *)
+
+val thread_flags = 0w1;
+
+fun load_word () : word =
+  RunCall.loadWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags);
+
+fun get_attributes () = Attributes (Word.andb (load_word (), thread_attributes));
 
-val private_interrupts =
-  [Thread.Thread.EnableBroadcastInterrupt false,
-    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
+fun set_attributes (Attributes w) =
+  let
+    val w' = Word.orb (Word.andb (load_word (), Word.notb thread_attributes), w);
+    val _ = RunCall.storeWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags, w');
+  in
+    if Word.andb (w', interrupt_asynch) = interrupt_asynch
+    then Thread.Thread.testInterrupt () else ()
+  end;
+
+fun convert_attributes (Attributes w) =
+  [Thread.Thread.EnableBroadcastInterrupt (Word.andb (w, broadcast) = broadcast),
+   Thread.Thread.InterruptState
+      let val w' = Word.andb (w, interrupt_state) in
+        if w' = interrupt_defer then Thread.Thread.InterruptDefer
+        else if w' = interrupt_synch then Thread.Thread.InterruptSynch
+        else if w' = interrupt_asynch then Thread.Thread.InterruptAsynch
+        else Thread.Thread.InterruptAsynchOnce
+      end];
+
 
-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);
+(* common configurations *)
+
+val no_interrupts = Attributes interrupt_defer;
+val test_interrupts = Attributes interrupt_synch;
+val public_interrupts = Attributes (Word.orb (broadcast, interrupt_asynch_once));
+val private_interrupts = Attributes interrupt_asynch_once;
 
-val safe_interrupts = map
-  (fn Thread.Thread.InterruptState Thread.Thread.InterruptAsynch =>
-      Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce
-    | x => x);
+fun sync_interrupts (Attributes w) =
+  let
+    val w' = Word.andb (w, interrupt_state);
+    val w'' = Word.andb (w, Word.notb interrupt_state);
+  in Attributes (if w' = interrupt_defer then w else Word.orb (w'', interrupt_synch)) end;
+
+fun safe_interrupts (Attributes w) =
+  let
+    val w' = Word.andb (w, interrupt_state);
+    val w'' = Word.andb (w, Word.notb interrupt_state);
+  in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
+
+end;
 
 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;
+    val orig_atts = safe_interrupts (get_attributes ());
+    val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) ();
+    val _ = set_attributes orig_atts;
   in Exn.release result end;
 
 fun uninterruptible f x =
@@ -63,10 +103,10 @@
 
 fun expose_interrupt () =
   let
-    val orig_atts = safe_interrupts (Thread.Thread.getAttributes ());
-    val _ = Thread.Thread.setAttributes test_interrupts;
+    val orig_atts = safe_interrupts (get_attributes ());
+    val _ = set_attributes test_interrupts;
     val test = Exn.capture Thread.Thread.testInterrupt ();
-    val _ = Thread.Thread.setAttributes orig_atts;
+    val _ = set_attributes orig_atts;
   in Exn.release test end;
 
 end;

--- a/src/Pure/Tools/ml_process.scala	Tue Dec 13 11:51:42 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala	Tue Dec 13 23:29:54 2016 +0100
@@ -48,7 +48,18 @@
           fun subparagraph (_: string) = ();
           val ML_file = PolyML.use;
           """,
-          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
+          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
+            """
+              structure FixedInt = IntInf;
+              structure RunCall =
+              struct
+                open RunCall
+                val loadWord: word * word -> word =
+                  run_call2 RuntimeCalls.POLY_SYS_load_word;
+                val storeWord: word * word * word -> unit =
+                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
+              end;
+            """
           else "",
           if (Platform.is_windows)
             "fun exit 0 = OS.Process.exit OS.Process.success" +