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