src/Pure/context.ML

   val join_certificate: certificate * certificate -> certificate
   (*generic context*)
   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,
     active_theories: int,
     active_proofs: int,

 (* heap allocations *)
 
 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 =
   Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens));