# 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 ***)