# HG changeset patch
# User wenzelm
# Date 1680185359 -7200
# Node ID 8db468bd1ec674a9413f901373fb8c9a1e7099c9
# Parent  44a6ac96314d467ba1253f4a069aa426c76ff914
more operations for profiling;

diff -r 44a6ac96314d -r 8db468bd1ec6 src/Pure/ML/ml_heap.ML
--- a/src/Pure/ML/ml_heap.ML	Thu Mar 30 16:04:02 2023 +0200
+++ b/src/Pure/ML/ml_heap.ML	Thu Mar 30 16:09:19 2023 +0200
@@ -8,6 +8,7 @@
 sig
   val obj_size: 'a -> int
   val sizeof1: 'a -> int
+  val sizeof_list: 'a list -> int
   val sizeof: 'a list -> int
   val full_gc: unit -> unit
   val gc_now: unit -> Time.time
@@ -21,7 +22,9 @@
 val obj_size = PolyML.objSize;
 
 fun sizeof1 x = obj_size x * ML_System.platform_obj_size;
-fun sizeof xs = (obj_size xs - 3 * length xs) * ML_System.platform_obj_size;
+
+fun sizeof_list xs = 3 * length xs * ML_System.platform_obj_size;
+fun sizeof xs = obj_size xs * ML_System.platform_obj_size - sizeof_list xs;
 
 val full_gc = PolyML.fullGC;