src/Pure/ML/ml_heap.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62825 e6e80a8bf624
child 67622 5289d3bdb261
permissions -rw-r--r--
more robust sorted_entries;
wenzelm@62508
     1
(*  Title:      Pure/ML/ml_heap.ML
wenzelm@62467
     2
    Author:     Makarius
wenzelm@62467
     3
wenzelm@62467
     4
ML heap operations.
wenzelm@62467
     5
*)
wenzelm@62467
     6
wenzelm@62467
     7
signature ML_HEAP =
wenzelm@62467
     8
sig
wenzelm@62825
     9
  val obj_size: 'a -> int
wenzelm@62467
    10
  val share_common_data: unit -> unit
wenzelm@62825
    11
  val save_child: string -> unit
wenzelm@62467
    12
end;
wenzelm@62467
    13
wenzelm@62467
    14
structure ML_Heap: ML_HEAP =
wenzelm@62467
    15
struct
wenzelm@62825
    16
wenzelm@62825
    17
val obj_size = PolyML.objSize;
wenzelm@62825
    18
wenzelm@62825
    19
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
wenzelm@62825
    20
wenzelm@62825
    21
fun save_child name =
wenzelm@62825
    22
  PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ()));
wenzelm@62825
    23
wenzelm@62467
    24
end;