# HG changeset patch # User wenzelm # Date 1683739817 -7200 # Node ID 1a829342a2d3816f20a4a1048594ccfeceb309d2 # Parent 82b09fd28504157207c450dc6465f1dbb79cbad1 clarified context tracing; proper finish: purge inactive entries; diff -r 82b09fd28504 -r 1a829342a2d3 src/Pure/PIDE/session.ML --- a/src/Pure/PIDE/session.ML Wed May 10 16:05:14 2023 +0200 +++ b/src/Pure/PIDE/session.ML Wed May 10 19:30:17 2023 +0200 @@ -40,6 +40,7 @@ (shutdown (); Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ()); Thy_Info.finish (); + Context.finish_tracing (); shutdown ()); end; diff -r 82b09fd28504 -r 1a829342a2d3 src/Pure/context.ML --- a/src/Pure/context.ML Wed May 10 16:05:14 2023 +0200 +++ b/src/Pure/context.ML Wed May 10 19:30:17 2023 +0200 @@ -69,7 +69,7 @@ datatype generic = Theory of theory | Proof of Proof.context val theory_tracing: bool Unsynchronized.ref val proof_tracing: bool Unsynchronized.ref - val allocations_trace: unit -> + val finish_tracing: unit -> {contexts: (generic * Position.T) list, active_contexts: int, active_theories: int, @@ -200,18 +200,27 @@ local +fun cons_tokens var token = + Synchronized.change var (fn (n, tokens) => (n + 1, Weak.weak (SOME token) :: tokens)); + +fun finish_tokens var = + Synchronized.change_result var (fn (n, tokens) => + let + val tokens' = filter Unsynchronized.weak_active tokens; + val results = map_filter Unsynchronized.weak_peek tokens'; + in ((n, results), (n, tokens')) end); + fun make_token guard var token0 = if ! guard then let val token = Unsynchronized.ref (! token0); val pos = Position.thread_data (); - fun assign res = - (token := res; Synchronized.change var (cons (Weak.weak (SOME token))); res); + fun assign res = (token := res; cons_tokens var token; res); in (token, pos, assign) end else (token0, Position.none, I); -val theory_tokens = Synchronized.var "theory_tokens" ([]: theory Unsynchronized.weak_ref list); -val proof_tokens = Synchronized.var "proof_tokens" ([]: Proof.context Unsynchronized.weak_ref list); +val theory_tokens = Synchronized.var "theory_tokens" (0, []: theory Unsynchronized.weak_ref list); +val proof_tokens = Synchronized.var "proof_tokens" (0, []: proof Unsynchronized.weak_ref list); val theory_token0 = Unsynchronized.ref Thy_Undef; val proof_token0 = Unsynchronized.ref Prf_Undef; @@ -221,29 +230,20 @@ 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 () = +fun finish_tracing () = let val _ = ML_Heap.full_gc (); - val trace1 = Synchronized.value theory_tokens; - val trace2 = Synchronized.value proof_tokens; + val (total_theories, token_theories) = finish_tokens theory_tokens; + val (total_proofs, token_proofs) = finish_tokens proof_tokens; - fun cons1 r = - (case Unsynchronized.weak_peek r of - SOME (thy as Thy (_, {theory_token_pos, ...}, _, _)) => - cons (Theory thy, theory_token_pos) - | _ => I); - fun cons2 r = - (case Unsynchronized.weak_peek r of - SOME (ctxt as Prf (_, proof_token_pos, _, _)) => - cons (Proof ctxt, proof_token_pos) - | _ => I); + fun cons1 (thy as Thy (_, {theory_token_pos, ...}, _, _)) = cons (Theory thy, theory_token_pos) + | cons1 _ = I; + fun cons2 (ctxt as Prf (_, proof_token_pos, _, _)) = cons (Proof ctxt, proof_token_pos) + | cons2 _ = I; - val contexts = build (fold cons1 trace1 #> fold cons2 trace2); + val contexts = build (fold cons1 token_theories #> fold cons2 token_proofs); val active_theories = fold (fn (Theory _, _) => Integer.add 1 | _ => I) contexts 0; val active_proofs = fold (fn (Proof _, _) => Integer.add 1 | _ => I) contexts 0; - - val total_theories = length trace1; - val total_proofs = length trace2; in {contexts = contexts, active_contexts = active_theories + active_proofs,