--- 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 =