src/Tools/nbe.ML
changeset 39388 fdbb2c55ffc2
parent 39290 44e4d8dfd6bf
child 39392 7a0fcee7a2a3
     1.1 --- a/src/Tools/nbe.ML	Wed Sep 15 11:30:31 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Sep 15 11:30:32 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4                                               (*abstractions as closures*)
     1.5    val same: Univ -> Univ -> bool
     1.6  
     1.7 -  val univs_ref: (unit -> Univ list -> Univ list) option Unsynchronized.ref
     1.8 +  val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
     1.9    val trace: bool Unsynchronized.ref
    1.10  
    1.11    val setup: theory -> theory
    1.12 @@ -228,10 +228,15 @@
    1.13  
    1.14  (* nbe specific syntax and sandbox communication *)
    1.15  
    1.16 -val univs_ref = Unsynchronized.ref (NONE : (unit -> Univ list -> Univ list) option);
    1.17 +structure Univs = Proof_Data(
    1.18 +  type T = unit -> Univ list -> Univ list
    1.19 +  fun init thy () = error "Univs"
    1.20 +);
    1.21 +val put_result = Univs.put;
    1.22  
    1.23  local
    1.24    val prefix =      "Nbe.";
    1.25 +  val name_put =    prefix ^ "put_result";
    1.26    val name_ref =    prefix ^ "univs_ref";
    1.27    val name_const =  prefix ^ "Const";
    1.28    val name_abss =   prefix ^ "abss";
    1.29 @@ -239,7 +244,7 @@
    1.30    val name_same =   prefix ^ "same";
    1.31  in
    1.32  
    1.33 -val univs_cookie = (name_ref, univs_ref);
    1.34 +val univs_cookie = (Univs.get, put_result, name_put);
    1.35  
    1.36  fun nbe_fun 0 "" = "nbe_value"
    1.37    | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
    1.38 @@ -389,7 +394,7 @@
    1.39          s
    1.40          |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
    1.41          |> pair ""
    1.42 -        |> ML_Context.evaluate ctxt (!trace) univs_cookie
    1.43 +        |> ML_Context.value ctxt univs_cookie
    1.44          |> (fn f => f deps_vals)
    1.45          |> (fn univs => cs ~~ univs)
    1.46        end;