# HG changeset patch
# User haftmann
# Date 1464269270 -7200
# Node ID 84c6dd947b751ff6213d1abbbcc5d0da6af09b3d
# Parent  534f16b0ca3975831ea1d652d6a3e603dd2e4a74
clarified proof context vs. background theory

diff -r 534f16b0ca39 -r 84c6dd947b75 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu May 26 15:27:50 2016 +0200
@@ -338,7 +338,7 @@
     val ((tycos, consts), _) = Code_Antiq_Data.get ctxt;
     val tycos' = fold (insert (op =)) new_tycos tycos;
     val consts' = fold (insert (op =)) new_consts consts;
-    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts';
+    val program = Code_Thingol.consts_program ctxt consts';
     val acc_code = Lazy.lazy (fn () =>
       evaluation_code ctxt structure_generated program tycos' consts'
       |> apsnd snd);
@@ -440,7 +440,7 @@
       |> apsnd flat;
     val functions = map (prep_const thy) raw_functions;
     val consts = constrs @ functions;
-    val program = Code_Thingol.consts_program (Proof_Context.theory_of ctxt) consts;
+    val program = Code_Thingol.consts_program ctxt consts;
     val result = evaluation_code ctxt module_name program tycos consts
       |> (apsnd o apsnd) (chop (length constrs));
   in
diff -r 534f16b0ca39 -r 84c6dd947b75 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_target.ML	Thu May 26 15:27:50 2016 +0200
@@ -429,8 +429,7 @@
 
 fun export_code ctxt all_public cs seris =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val program = Code_Thingol.consts_program thy cs;
+    val program = Code_Thingol.consts_program ctxt cs;
     val _ = map (fn (((target_name, module_name), some_path), args) =>
       export_code_for ctxt some_path target_name NONE module_name args program all_public (map Constant cs)) seris;
   in () end;
@@ -442,20 +441,17 @@
 
 fun produce_code ctxt all_public cs target_name some_width some_module_name args =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val program = Code_Thingol.consts_program thy cs;
+    val program = Code_Thingol.consts_program ctxt cs;
   in produce_code_for ctxt target_name some_width some_module_name args program all_public (map Constant cs) end;
 
 fun present_code ctxt cs syms target_name some_width some_module_name args =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val program = Code_Thingol.consts_program thy cs;
+    val program = Code_Thingol.consts_program ctxt cs;
   in present_code_for ctxt target_name some_width some_module_name args program (map Constant cs, syms) end;
 
 fun check_code ctxt all_public cs seris =
   let
-    val thy = Proof_Context.theory_of ctxt;
-    val program = Code_Thingol.consts_program thy cs;
+    val program = Code_Thingol.consts_program ctxt cs;
     val _ = map (fn ((target_name, strict), args) =>
       check_code_for ctxt target_name strict args program all_public (map Constant cs)) seris;
   in () end;
diff -r 534f16b0ca39 -r 84c6dd947b75 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu May 26 15:27:50 2016 +0200
@@ -84,7 +84,7 @@
       * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
 
   val read_const_exprs: Proof.context -> string list -> string list
-  val consts_program: theory -> string list -> program
+  val consts_program: Proof.context -> string list -> program
   val dynamic_conv: Proof.context -> (program
     -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> conv
@@ -776,22 +776,23 @@
   val empty = Code_Symbol.Graph.empty;
 );
 
-fun invoke_generation ignore_cache thy (algebra, eqngr) generate thing =
-  Program.change_yield (if ignore_cache then NONE else SOME thy)
+fun invoke_generation ignore_cache ctxt (algebra, eqngr) generate thing =
+  Program.change_yield
+    (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
     (fn program => ([], program)
-      |> generate (Proof_Context.init_global thy) algebra eqngr thing
+      |> generate ctxt algebra eqngr thing
       |-> (fn thing => fn (_, program) => (thing, program)));
 
 
 (* program generation *)
 
-fun consts_program_internal thy permissive consts =
+fun consts_program_internal ctxt permissive consts =
   let
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr permissive);
   in
-    invoke_generation permissive thy
-      (Code_Preproc.obtain false (Proof_Context.init_global thy) consts [])
+    invoke_generation permissive ctxt
+      (Code_Preproc.obtain false ctxt consts [])
       generate_consts consts
     |> snd
   end;
@@ -842,7 +843,7 @@
 fun dynamic_evaluation eval ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
-      invoke_generation false (Proof_Context.theory_of ctxt)
+      invoke_generation false ctxt
         (algebra, eqngr) ensure_value t;
   in eval program t vs_ty_t' deps end;
 
@@ -859,7 +860,7 @@
     fun generate_consts ctxt algebra eqngr =
       fold_map (ensure_const ctxt algebra eqngr false);
     val (deps, program) =
-      invoke_generation true (Proof_Context.theory_of ctxt)
+      invoke_generation true ctxt
         (algebra, eqngr) generate_consts consts;
   in static_eval { program = program, deps = deps } end;
 
@@ -919,9 +920,10 @@
 
 fun read_const_exprs ctxt const_exprs =
   let
-    val (consts, consts_permissive) = read_const_exprs_internal ctxt const_exprs;
+    val (consts, consts_permissive) =
+      read_const_exprs_internal ctxt const_exprs;
     val consts' = implemented_deps
-      (consts_program_permissive (Proof_Context.theory_of ctxt) consts_permissive);
+      (consts_program_permissive ctxt consts_permissive);
   in union (op =) consts' consts end;