# HG changeset patch
# User wenzelm
# Date 1210769018 -7200
# Node ID f9ec18f7c0f6bcfd40b81de0cb958b9e903ffbc8
# Parent  ccea41fb5c39da7d6be598f992d0f41715415f27
setmp_thread_data: do nothing if Output.debugging;

diff -r ccea41fb5c39 -r f9ec18f7c0f6 src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Wed May 14 14:43:37 2008 +0200
+++ b/src/Pure/General/position.ML	Wed May 14 14:43:38 2008 +0200
@@ -102,7 +102,10 @@
 local val tag = Universal.tag () : T Universal.tag in
 
 fun thread_data () = the_default none (Multithreading.get_data tag);
-fun setmp_thread_data pos = Library.setmp_thread_data tag (thread_data ()) pos;
+
+fun setmp_thread_data pos f x =
+  if ! Output.debugging then f x
+  else Library.setmp_thread_data tag (thread_data ()) pos f x;
 
 fun setmp_thread_data_seq pos f seq =
   setmp_thread_data pos f seq |> Seq.wrap (fn pull => setmp_thread_data pos pull ());