equal
deleted
inserted
replaced
100 (* thread data *) |
100 (* thread data *) |
101 |
101 |
102 local val tag = Universal.tag () : T Universal.tag in |
102 local val tag = Universal.tag () : T Universal.tag in |
103 |
103 |
104 fun thread_data () = the_default none (Multithreading.get_data tag); |
104 fun thread_data () = the_default none (Multithreading.get_data tag); |
105 fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos; |
105 |
|
106 fun setmp_thread_data pos f x = |
|
107 if ! Output.debugging then f x |
|
108 else Library.setmp_thread_data tag (thread_data ()) pos f x; |
106 |
109 |
107 fun setmp_thread_data_seq pos f seq = |
110 fun setmp_thread_data_seq pos f seq = |
108 setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ()); |
111 setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ()); |
109 |
112 |
110 end; |
113 end; |