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