author | wenzelm |
Sun, 20 May 2018 15:37:16 +0200 | |
changeset 68231 | 0004e7a9fa10 |
parent 67622 | 5289d3bdb261 |
child 69826 | 1bea05713dde |
permissions | -rw-r--r-- |
(* Title: Pure/ML/ml_heap.ML Author: Makarius ML heap operations. *) signature ML_HEAP = sig val obj_size: 'a -> int val full_gc: unit -> unit val share_common_data: unit -> unit val save_child: string -> unit end; structure ML_Heap: ML_HEAP = struct val obj_size = PolyML.objSize; val full_gc = PolyML.fullGC; fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; fun save_child name = PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ())); end;