# HG changeset patch
# User wenzelm
# Date 1683726229 -7200
# Node ID dfa44d85d751606e6394343cd11bb012c283ebd6
# Parent  db041670d6bbe6464baae019e59a9d35b2697789
proper system options to control context tracing/timing;

diff -r db041670d6bb -r dfa44d85d751 etc/options
--- a/etc/options	Wed May 10 08:59:44 2023 +0200
+++ b/etc/options	Wed May 10 15:43:49 2023 +0200
@@ -111,6 +111,15 @@
 public option timeout_scale : real = 1.0 for build
   -- "scale factor for timeout in Isabelle/ML and session build"
 
+option context_data_timing : bool = false for build
+  -- "timing for context data operations"
+
+option context_theory_tracing : bool = false for build
+  -- "tracing of persistent theory values within ML heap"
+
+option context_proof_tracing : bool = false for build
+  -- "tracing of persistent Proof.context values within ML heap"
+
 
 section "Detail of Proof Checking"
 
diff -r db041670d6bb -r dfa44d85d751 src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Wed May 10 08:59:44 2023 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed May 10 15:43:49 2023 +0200
@@ -200,7 +200,10 @@
   if Options.default_bool "export_standard_proofs" then Proofterm.proofs := 2 else ();
   let val proofs = Options.default_int "record_proofs"
   in if proofs < 0 then () else Proofterm.proofs := proofs end;
-  Printer.show_markup_default := false);
+  Printer.show_markup_default := false;
+  Context.theory_tracing := Options.default_bool "context_theory_tracing";
+  Context.proof_tracing := Options.default_bool "context_proof_tracing";
+  Context.data_timing := Options.default_bool "context_data_timing");
 
 fun init_options_interactive () =
  (init_options ();
diff -r db041670d6bb -r dfa44d85d751 src/Pure/context.ML
--- a/src/Pure/context.ML	Wed May 10 08:59:44 2023 +0200
+++ b/src/Pure/context.ML	Wed May 10 15:43:49 2023 +0200
@@ -34,7 +34,7 @@
   type id = int
   type theory_id
   val theory_id: theory -> theory_id
-  val timing: bool Unsynchronized.ref
+  val data_timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
   val theory_id_ord: theory_id ord
@@ -67,8 +67,8 @@
   val join_certificate: certificate * certificate -> certificate
   (*generic context*)
   datatype generic = Theory of theory | Proof of Proof.context
-  val trace_theories: bool Unsynchronized.ref
-  val trace_proofs: bool Unsynchronized.ref
+  val theory_tracing: bool Unsynchronized.ref
+  val proof_tracing: bool Unsynchronized.ref
   val allocations_trace: unit ->
    {contexts: (generic * Position.T) list,
     active_contexts: int,
@@ -195,8 +195,8 @@
 
 (* heap allocations *)
 
-val trace_theories = Unsynchronized.ref false;
-val trace_proofs = Unsynchronized.ref false;
+val theory_tracing = Unsynchronized.ref false;
+val proof_tracing = Unsynchronized.ref false;
 
 local
 
@@ -218,8 +218,8 @@
 
 in
 
-fun theory_token () = make_token trace_theories theory_tokens theory_token0;
-fun proof_token () = make_token trace_proofs proof_tokens proof_token0;
+fun theory_token () = make_token theory_tracing theory_tokens theory_token0;
+fun proof_token () = make_token proof_tracing proof_tokens proof_token0;
 
 fun allocations_trace () =
   let
@@ -368,7 +368,7 @@
 
 (* data kinds and access methods *)
 
-val timing = Unsynchronized.ref false;
+val data_timing = Unsynchronized.ref false;
 
 local
 
@@ -393,7 +393,7 @@
 val invoke_empty = #empty o the_kind;
 
 fun invoke_merge kind args =
-  if ! timing then
+  if ! data_timing then
     Timing.cond_timeit true ("Theory_Data.merge" ^ Position.here (#pos kind))
       (fn () => #merge kind args)
   else #merge kind args;