setmp_thread_data: do nothing if Output.debugging;
authorwenzelm
Wed, 14 May 2008 14:43:38 +0200
changeset 26890f9ec18f7c0f6
parent 26889 ccea41fb5c39
child 26891 bfa1944e5238
setmp_thread_data: do nothing if Output.debugging;
src/Pure/General/position.ML
     1.1 --- a/src/Pure/General/position.ML	Wed May 14 14:43:37 2008 +0200
     1.2 +++ b/src/Pure/General/position.ML	Wed May 14 14:43:38 2008 +0200
     1.3 @@ -102,7 +102,10 @@
     1.4  local val tag = Universal.tag () : T Universal.tag in
     1.5  
     1.6  fun thread_data () = the_default none (Multithreading.get_data tag);
     1.7 -fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
     1.8 +
     1.9 +fun setmp_thread_data pos f x =
    1.10 +  if ! Output.debugging then f x
    1.11 +  else Library.setmp_thread_data tag (thread_data ()) pos f x;
    1.12  
    1.13  fun setmp_thread_data_seq pos f seq =
    1.14    setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ());