src/Pure/ML/ml_heap.ML
author wenzelm
Mon, 27 Aug 2018 14:42:24 +0200
changeset 68816 5a53724fe247
parent 67622 5289d3bdb261
child 69826 1bea05713dde
permissions -rw-r--r--
support named ML environments, notably "Isabelle", "SML"; more uniform options ML_read_global, ML_write_global; clarified bootstrap environment;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
62508
d0b68218ea55 discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents: 62468
diff changeset
     1
(*  Title:      Pure/ML/ml_heap.ML
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     3
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     4
ML heap operations.
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     5
*)
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     6
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     7
signature ML_HEAP =
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
     8
sig
62825
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
     9
  val obj_size: 'a -> int
67622
5289d3bdb261 more operations;
wenzelm
parents: 62825
diff changeset
    10
  val full_gc: unit -> unit
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    11
  val share_common_data: unit -> unit
62825
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    12
  val save_child: string -> unit
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    13
end;
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    14
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    15
structure ML_Heap: ML_HEAP =
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    16
struct
62825
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    17
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    18
val obj_size = PolyML.objSize;
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    19
67622
5289d3bdb261 more operations;
wenzelm
parents: 62825
diff changeset
    20
val full_gc = PolyML.fullGC;
5289d3bdb261 more operations;
wenzelm
parents: 62825
diff changeset
    21
62825
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    22
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    23
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    24
fun save_child name =
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    25
  PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ()));
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents: 62630
diff changeset
    26
62467
c1b88e647e2f clarified ML heap operations;
wenzelm
parents:
diff changeset
    27
end;