isabelle: src/Pure/ML/ml_recursive.ML@572ab9e64e18 (annotated)

62910 f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	1	(* Title: Pure/ML/ml_recursive.ML
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	2	Author: Makarius
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	3
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	4	ML name space for recursive compiler invocation.
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	5	*)
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	6
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	7	signature ML_RECURSIVE =
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	8	sig
62941 5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	9	type env =
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	10	{debug: bool,
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	11	name_space: PolyML.NameSpace.nameSpace,
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	12	add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit};
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	13	val get: unit -> env option
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	14	val recursive: env -> (unit -> 'a) -> 'a
62910 f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	15	end;
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	16
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	17	structure ML_Recursive: ML_RECURSIVE =
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	18	struct
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	19
62941 5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	20	type env =
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	21	{debug: bool,
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	22	name_space: PolyML.NameSpace.nameSpace,
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	23	add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit};
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	24
5612ec9f0f49 proper support for recursive ML debugging; wenzelm parents: 62910 diff changeset	25	val var = Thread_Data.var () : env Thread_Data.var;
62910 f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	26
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	27	fun get () = Thread_Data.get var;
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	28	fun recursive space e = Thread_Data.setmp var (SOME space) e ();
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	29
f37878ebba65 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; wenzelm parents: diff changeset	30	end;

author	haftmann
	Wed, 05 Feb 2020 20:17:00 +0000
changeset 71420	572ab9e64e18
parent 62941	5612ec9f0f49
permissions	-rw-r--r--