src/Pure/ML/ml_recursive.ML

--- a/src/Pure/ML/ml_recursive.ML	Sun Apr 10 17:52:30 2016 +0200
+++ b/src/Pure/ML/ml_recursive.ML	Sun Apr 10 18:41:49 2016 +0200
@@ -6,14 +6,23 @@
 
 signature ML_RECURSIVE =
 sig
-  val get: unit -> PolyML.NameSpace.nameSpace option
-  val recursive: PolyML.NameSpace.nameSpace -> (unit -> 'a) -> 'a
+  type env =
+    {debug: bool,
+     name_space: PolyML.NameSpace.nameSpace,
+     add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit};
+  val get: unit -> env option
+  val recursive: env -> (unit -> 'a) -> 'a
 end;
 
 structure ML_Recursive: ML_RECURSIVE =
 struct
 
-val var = Thread_Data.var () : PolyML.NameSpace.nameSpace Thread_Data.var;
+type env =
+  {debug: bool,
+   name_space: PolyML.NameSpace.nameSpace,
+   add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit};
+
+val var = Thread_Data.var () : env Thread_Data.var;
 
 fun get () = Thread_Data.get var;
 fun recursive space e = Thread_Data.setmp var (SOME space) e ();