tuned scope of lazy computation
authorhaftmann
Thu, 26 Jan 2017 16:06:18 +0100
changeset 64956 de7ce0fad5bc
parent 64955 25281bee02ac
child 64957 3faa9b31ff78
tuned scope of lazy computation
src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
+++ b/src/Tools/Code/code_runtime.ML	Thu Jan 26 16:06:18 2017 +0100
@@ -418,8 +418,9 @@
 
 val is_first_occurrence = #first_occurrence o Code_Antiq_Data.get;
 
-fun lazy_code ctxt program consts = Lazy.lazy (fn () =>
+fun lazy_code ctxt consts = Lazy.lazy (fn () =>
   let
+    val program = Code_Thingol.consts_program ctxt consts;
     val (code, (_, consts_map)) =
       evaluation_code ctxt Code_Target.generatedN program [] consts
   in { code = code, consts_map = consts_map } end);
@@ -427,13 +428,12 @@
 fun register_const const ctxt =
   let
     val consts = insert (op =) const ((#named_consts o Code_Antiq_Data.get) ctxt);
-    val program = Code_Thingol.consts_program ctxt consts;
   in
     ctxt
     |> Code_Antiq_Data.put { 
         named_consts = consts,
         first_occurrence = false,
-        generated_code = lazy_code ctxt program consts
+        generated_code = lazy_code ctxt consts
       }
   end;