src/Pure/ML/ml_recursive.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_recursive.ML	Thu Apr 07 21:27:17 2016 +0200
@@ -0,0 +1,21 @@
+(*  Title:      Pure/ML/ml_recursive.ML
+    Author:     Makarius
+
+ML name space for recursive compiler invocation.
+*)
+
+signature ML_RECURSIVE =
+sig
+  val get: unit -> PolyML.NameSpace.nameSpace option
+  val recursive: PolyML.NameSpace.nameSpace -> (unit -> 'a) -> 'a
+end;
+
+structure ML_Recursive: ML_RECURSIVE =
+struct
+
+val var = Thread_Data.var () : PolyML.NameSpace.nameSpace Thread_Data.var;
+
+fun get () = Thread_Data.get var;
+fun recursive space e = Thread_Data.setmp var (SOME space) e ();
+
+end;