| author | wenzelm |
| Thu, 07 Apr 2016 21:27:17 +0200 | |
| changeset 62910 | f37878ebba65 |
| child 62941 | 5612ec9f0f49 |
| permissions | -rw-r--r-- |
|
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 |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
9 |
val get: unit -> PolyML.NameSpace.nameSpace option |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
10 |
val recursive: PolyML.NameSpace.nameSpace -> (unit -> 'a) -> 'a |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
11 |
end; |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
12 |
|
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
13 |
structure ML_Recursive: ML_RECURSIVE = |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
14 |
struct |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
15 |
|
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
16 |
val var = Thread_Data.var () : PolyML.NameSpace.nameSpace Thread_Data.var; |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
17 |
|
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
18 |
fun get () = Thread_Data.get var; |
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
19 |
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
|
20 |
|
|
f37878ebba65
explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
wenzelm
parents:
diff
changeset
|
21 |
end; |