Thread.getLocal/setLocal;
authorwenzelm
Thu Sep 04 16:03:44 2008 +0200 (2008-09-04)
changeset 281223d099ce624e7
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
     1.1 --- a/src/Pure/General/position.ML	Thu Sep 04 16:03:43 2008 +0200
     1.2 +++ b/src/Pure/General/position.ML	Thu Sep 04 16:03:44 2008 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  
     1.5  local val tag = Universal.tag () : T Universal.tag in
     1.6  
     1.7 -fun thread_data () = the_default none (Multithreading.get_data tag);
     1.8 +fun thread_data () = the_default none (Thread.getLocal tag);
     1.9  
    1.10  fun setmp_thread_data pos f x =
    1.11    if ! Output.debugging then f x
     2.1 --- a/src/Pure/General/print_mode.ML	Thu Sep 04 16:03:43 2008 +0200
     2.2 +++ b/src/Pure/General/print_mode.ML	Thu Sep 04 16:03:44 2008 +0200
     2.3 @@ -34,7 +34,7 @@
     2.4  
     2.5  fun print_mode_value () =
     2.6    let val modes =
     2.7 -    (case Multithreading.get_data tag of
     2.8 +    (case Thread.getLocal tag of
     2.9        SOME (SOME modes) => modes
    2.10      | _ => NAMED_CRITICAL "print_mode" (fn () => ! print_mode))
    2.11    in subtract (op =) [input, internal] modes end;
    2.12 @@ -42,7 +42,7 @@
    2.13  fun print_mode_active mode = member (op =) (print_mode_value ()) mode;
    2.14  
    2.15  fun setmp modes f x =
    2.16 -  let val orig_modes = (case Multithreading.get_data tag of SOME (SOME ms) => SOME ms | _ => NONE)
    2.17 +  let val orig_modes = (case Thread.getLocal tag of SOME (SOME ms) => SOME ms | _ => NONE)
    2.18    in setmp_thread_data tag orig_modes (SOME modes) f x end;
    2.19  
    2.20  fun with_modes modes f x = setmp (modes @ print_mode_value ()) f x;
     3.1 --- a/src/Pure/context.ML	Thu Sep 04 16:03:43 2008 +0200
     3.2 +++ b/src/Pure/context.ML	Thu Sep 04 16:03:44 2008 +0200
     3.3 @@ -512,7 +512,7 @@
     3.4  local val tag = Universal.tag () : generic option Universal.tag in
     3.5  
     3.6  fun thread_data () =
     3.7 -  (case Multithreading.get_data tag of
     3.8 +  (case Thread.getLocal tag of
     3.9      SOME (SOME context) => SOME context
    3.10    | _ => NONE);
    3.11  
    3.12 @@ -521,7 +521,7 @@
    3.13      SOME context => context
    3.14    | _ => error "Unknown context");
    3.15  
    3.16 -fun set_thread_data context = Multithreading.put_data (tag, context);
    3.17 +fun set_thread_data context = Thread.setLocal (tag, context);
    3.18  fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
    3.19  
    3.20  end;
     4.1 --- a/src/Pure/library.ML	Thu Sep 04 16:03:43 2008 +0200
     4.2 +++ b/src/Pure/library.ML	Thu Sep 04 16:03:44 2008 +0200
     4.3 @@ -346,9 +346,9 @@
     4.4  fun setmp_thread_data tag orig_data data f x =
     4.5    uninterruptible (fn restore_attributes => fn () =>
     4.6      let
     4.7 -      val _ = Multithreading.put_data (tag, data);
     4.8 +      val _ = Thread.setLocal (tag, data);
     4.9        val result = Exn.capture (restore_attributes f) x;
    4.10 -      val _ = Multithreading.put_data (tag, orig_data);
    4.11 +      val _ = Thread.setLocal (tag, orig_data);
    4.12      in Exn.release result end) ();
    4.13  
    4.14