more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
authorwenzelm
Fri, 21 May 2010 18:10:19 +0200
changeset 37043 f8e24980af05
parent 37042 55efdc260182
child 37044 d93b849cbecd
more robust Position.setmp_thread_data, independently of Output.debugging (essentially reverts f9ec18f7c0f6, which was motivated by clean exception_trace, but without transaction positions the Isabelle_Process protocol breaks down);
src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Fri May 21 17:26:42 2010 +0200
+++ b/src/Pure/General/position.ML	Fri May 21 18:10:19 2010 +0200
@@ -173,9 +173,7 @@
 
 fun thread_data () = the_default none (Thread.getLocal tag);
 
-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 pos = Library.setmp_thread_data tag (thread_data ()) pos;
 
 end;