# HG changeset patch # User wenzelm # Date 1518710905 -3600 # Node ID 8f93d878f8552743905cd973718d7ccdf5c3c18c # Parent 967213048e55e0f9c69ce33dec59e3ce1b377f0f auxiliary operation for space profiling; diff -r 967213048e55 -r 8f93d878f855 src/Pure/context.ML --- a/src/Pure/context.ML Thu Feb 15 14:36:46 2018 +0100 +++ b/src/Pure/context.ML Thu Feb 15 17:08:25 2018 +0100 @@ -50,6 +50,7 @@ val subthy: theory * theory -> bool val finish_thy: theory -> theory val begin_thy: string -> theory list -> theory + val theory_data_size: theory -> (Position.T * int) list (*proof context*) val raw_transfer: theory -> Proof.context -> Proof.context (*certificate*) @@ -265,6 +266,7 @@ in +fun invoke_pos k = invoke "" (K o #pos) k (); fun invoke_empty k = invoke "" (K o #empty) k (); val invoke_extend = invoke "extend" #extend; fun invoke_merge thys = invoke "merge" (fn kind => #merge kind thys); @@ -369,8 +371,17 @@ fun put k mk x = update_thy (Datatab.update (k, mk x)); +fun obj_size k thy = + Datatab.lookup (data_of thy) k |> Option.map ML_Heap.obj_size; + end; +fun theory_data_size thy = + (data_of thy, []) |-> Datatab.fold_rev (fn (k, _) => + (case Theory_Data.obj_size k thy of + NONE => I + | SOME n => (cons (invoke_pos k, n)))); + (*** proof context ***)