Thread.getLocal/setLocal;
authorwenzelm
Thu, 04 Sep 2008 16:03:44 +0200
changeset 28122 3d099ce624e7
parent 28121 2303b4c53d3a
child 28123 53cd972d7db9
Thread.getLocal/setLocal;
src/Pure/General/position.ML
src/Pure/General/print_mode.ML
src/Pure/context.ML
src/Pure/library.ML
--- a/src/Pure/General/position.ML	Thu Sep 04 16:03:43 2008 +0200
+++ b/src/Pure/General/position.ML	Thu Sep 04 16:03:44 2008 +0200
@@ -161,7 +161,7 @@
 
 local val tag = Universal.tag () : T Universal.tag in
 
-fun thread_data () = the_default none (Multithreading.get_data tag);
+fun thread_data () = the_default none (Thread.getLocal tag);
 
 fun setmp_thread_data pos f x =
   if ! Output.debugging then f x
--- a/src/Pure/General/print_mode.ML	Thu Sep 04 16:03:43 2008 +0200
+++ b/src/Pure/General/print_mode.ML	Thu Sep 04 16:03:44 2008 +0200
@@ -34,7 +34,7 @@
 
 fun print_mode_value () =
   let val modes =
-    (case Multithreading.get_data tag of
+    (case Thread.getLocal tag of
       SOME (SOME modes) => modes
     | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
   in subtract (op =) [input, internal] modes end;
@@ -42,7 +42,7 @@
 fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
 
 fun setmp modes f x =
-  let val orig_modes = (case Multithreading.get_data tag of SOME (SOME ms) => SOME ms | _ => NONE)
+  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
   in setmp_thread_data tag orig_modes (SOME modes) f x end;
 
 fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
--- a/src/Pure/context.ML	Thu Sep 04 16:03:43 2008 +0200
+++ b/src/Pure/context.ML	Thu Sep 04 16:03:44 2008 +0200
@@ -512,7 +512,7 @@
 local val tag = Universal.tag () : generic option Universal.tag in
 
 fun thread_data () =
-  (case Multithreading.get_data tag of
+  (case Thread.getLocal tag of
     SOME (SOME context) => SOME context
   | _ => NONE);
 
@@ -521,7 +521,7 @@
     SOME context => context
   | _ => error "Unknown context");
 
-fun set_thread_data context = Multithreading.put_data (tag, context);
+fun set_thread_data context = Thread.setLocal (tag, context);
 fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
 
 end;
--- a/src/Pure/library.ML	Thu Sep 04 16:03:43 2008 +0200
+++ b/src/Pure/library.ML	Thu Sep 04 16:03:44 2008 +0200
@@ -346,9 +346,9 @@
 fun setmp_thread_data tag orig_data data f x =
   uninterruptible (fn restore_attributes => fn () =>
     let
-      val _ = Multithreading.put_data (tag, data);
+      val _ = Thread.setLocal (tag, data);
       val result = Exn.capture (restore_attributes f) x;
-      val _ = Multithreading.put_data (tag, orig_data);
+      val _ = Thread.setLocal (tag, orig_data);
     in Exn.release result end) ();