isabelle: src/Pure/ML/ml_heap.ML@aa6a36c730c9 (annotated)

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
69826 1bea05713dde physical vs. logical events, the latter takes GC time into account; wenzelm parents: 67622 diff changeset	11	val gc_now: unit -> Time.time
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	12	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	13	val save_child: string -> unit
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	14	end;
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	15
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	16	structure ML_Heap: ML_HEAP =
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	17	struct
62825 e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	18
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	19	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	20
67622 5289d3bdb261 more operations; wenzelm parents: 62825 diff changeset	21	val full_gc = PolyML.fullGC;
5289d3bdb261 more operations; wenzelm parents: 62825 diff changeset	22
69826 1bea05713dde physical vs. logical events, the latter takes GC time into account; wenzelm parents: 67622 diff changeset	23	fun gc_now () = #timeGCReal (PolyML.Statistics.getLocalStats ());
1bea05713dde physical vs. logical events, the latter takes GC time into account; wenzelm parents: 67622 diff changeset	24
62825 e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	25	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	26
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	27	fun save_child name =
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	28	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	29
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	30	end;

author	wenzelm
	Wed, 15 Jul 2020 12:43:36 +0200
changeset 72037	aa6a36c730c9
parent 69826	1bea05713dde
child 77692	3e746e684f4b
permissions	-rw-r--r--