diff -r 37085099e415 -r bd5f6cee8001 src/Pure/context.ML
--- a/src/Pure/context.ML	Thu May 11 14:17:24 2023 +0200
+++ b/src/Pure/context.ML	Thu May 11 21:32:22 2023 +0200
@@ -69,6 +69,7 @@
   datatype generic = Theory of theory | Proof of Proof.context
   val theory_tracing: bool Unsynchronized.ref
   val proof_tracing: bool Unsynchronized.ref
+  val enabled_tracing: unit -> bool
   val finish_tracing: unit ->
    {contexts: (generic * Position.T) list,
     active_contexts: int,
@@ -198,6 +199,8 @@
 val theory_tracing = Unsynchronized.ref false;
 val proof_tracing = Unsynchronized.ref false;
 
+fun enabled_tracing () = ! theory_tracing orelse ! proof_tracing;
+
 local
 
 fun cons_tokens var token =