src/Pure/ML/ml_recursive.ML
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (20 months ago)
changeset 67003 49850a679c2c
parent 62941 5612ec9f0f49
permissions -rw-r--r--
more robust sorted_entries;
     1 (*  Title:      Pure/ML/ml_recursive.ML
     2     Author:     Makarius
     3 
     4 ML name space for recursive compiler invocation.
     5 *)
     6 
     7 signature ML_RECURSIVE =
     8 sig
     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
    15 end;
    16 
    17 structure ML_Recursive: ML_RECURSIVE =
    18 struct
    19 
    20 type env =
    21   {debug: bool,
    22    name_space: PolyML.NameSpace.nameSpace,
    23    add_breakpoints: (int * (bool ref * Thread_Position.T)) list -> unit};
    24 
    25 val var = Thread_Data.var () : env Thread_Data.var;
    26 
    27 fun get () = Thread_Data.get var;
    28 fun recursive space e = Thread_Data.setmp var (SOME space) e ();
    29 
    30 end;