diff -r a03592aafadf -r 5612ec9f0f49 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 ();