isabelle: src/Pure/ML/ml_heap.ML@630eaf8fe9f3 (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
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	10	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	11	val save_child: string -> unit
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	12	end;
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	13
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	14	structure ML_Heap: ML_HEAP =
c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	15	struct
62825 e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	16
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	17	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	18
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	19	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	20
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	21	fun save_child name =
e6e80a8bf624 structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle; wenzelm parents: 62630 diff changeset	22	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	23
62467 c1b88e647e2f clarified ML heap operations; wenzelm parents: diff changeset	24	end;

author	wenzelm
	Wed, 14 Sep 2016 12:51:40 +0200
changeset 63866	630eaf8fe9f3
parent 62825	e6e80a8bf624
child 67622	5289d3bdb261
permissions	-rw-r--r--