# HG changeset patch
# User haftmann
# Date 1262617224 -3600
# Node ID cd642bb91f64fe910e16e55a0f6a57444518d42b
# Parent  3b619abaa67a441f18ce0a23a8f6b02408ae52a7
code cache only persists on equal theories

diff -r 3b619abaa67a -r cd642bb91f64 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jan 04 16:00:23 2010 +0100
+++ b/src/Pure/Isar/code.ML	Mon Jan 04 16:00:24 2010 +0100
@@ -76,8 +76,8 @@
 signature CODE_DATA =
 sig
   type T
-  val change: theory -> (theory -> T -> T) -> T
-  val change_yield: theory -> (theory -> T -> 'a * T) -> 'a * T
+  val change: theory -> (T -> T) -> T
+  val change_yield: theory -> (T -> 'a * T) -> 'a * T
 end;
 
 signature PRIVATE_CODE =
@@ -85,9 +85,9 @@
   include CODE
   val declare_data: Object.T -> serial
   val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> (theory -> 'a -> 'a) -> 'a
+    -> theory -> ('a -> 'a) -> 'a
   val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> (theory -> 'a -> 'b * 'a) -> 'b * 'a
+    -> theory -> ('a -> 'b * 'a) -> 'b * 'a
 end;
 
 structure Code : PRIVATE_CODE =
@@ -287,18 +287,20 @@
 fun change_yield_data (kind, mk, dest) theory f =
   let
     val dataref = (snd o Code_Data.get) theory;
-    val (datatab, thy, thy_ref) = case Synchronized.value dataref
-     of SOME (datatab, thy_ref) => (datatab, Theory.deref thy_ref, thy_ref)
-      | NONE => (Datatab.empty, theory, Theory.check_thy theory)
+    val (datatab, thy_ref) = case Synchronized.value dataref
+     of SOME (datatab, thy_ref) => if Theory.eq_thy (theory, Theory.deref thy_ref)
+          then (datatab, thy_ref)
+          else (Datatab.empty, Theory.check_thy theory)
+      | NONE => (Datatab.empty, Theory.check_thy theory)
     val data = case Datatab.lookup datatab kind
      of SOME data => data
       | NONE => invoke_init kind;
-    val result as (x, data') = f thy (dest data);
+    val result as (x, data') = f (dest data);
     val _ = Synchronized.change dataref
       ((K o SOME) (Datatab.update (kind, mk data') datatab, thy_ref));
   in result end;
 
-fun change_data ops theory f = change_yield_data ops theory (pair () oo f) |> snd;
+fun change_data ops theory f = change_yield_data ops theory (f #> pair ()) |> snd;
 
 end; (*local*)
 
diff -r 3b619abaa67a -r cd642bb91f64 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Mon Jan 04 16:00:23 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML	Mon Jan 04 16:00:24 2010 +0100
@@ -282,7 +282,7 @@
    of SOME classess => (classess, ([], []))
     | NONE => let
         val all_classes = complete_proper_sort thy [class];
-        val superclasses = remove (op =) class all_classes
+        val superclasses = remove (op =) class all_classes;
         val classess = map (complete_proper_sort thy)
           (Sign.arity_sorts thy tyco [class]);
         val inst_params = inst_params thy tyco all_classes;
@@ -454,8 +454,8 @@
 
 (** retrieval and evaluation interfaces **)
 
-fun obtain theory cs ts = apsnd snd
-  (Wellsorted.change_yield theory (fn thy => extend_arities_eqngr thy cs ts));
+fun obtain thy cs ts = apsnd snd
+  (Wellsorted.change_yield thy (extend_arities_eqngr thy cs ts));
 
 fun gen_eval thy cterm_of conclude_evaluation evaluator proto_ct =
   let
diff -r 3b619abaa67a -r cd642bb91f64 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Jan 04 16:00:23 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Jan 04 16:00:24 2010 +0100
@@ -848,8 +848,8 @@
   val empty = (empty_naming, Graph.empty);
 );
 
-fun invoke_generation theory (algebra, eqngr) f name =
-  Program.change_yield theory (fn thy => fn naming_program => (NONE, naming_program)
+fun invoke_generation thy (algebra, eqngr) f name =
+  Program.change_yield thy (fn naming_program => (NONE, naming_program)
     |> f thy algebra eqngr name
     |-> (fn name => fn (_, naming_program) => (name, naming_program)));
 
diff -r 3b619abaa67a -r cd642bb91f64 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Mon Jan 04 16:00:23 2010 +0100
+++ b/src/Tools/nbe.ML	Mon Jan 04 16:00:24 2010 +0100
@@ -513,14 +513,15 @@
 
 (* compilation, evaluation and reification *)
 
-fun compile_eval theory naming program vs_t deps =
+fun compile_eval thy naming program vs_t deps =
   let
+    val ctxt = ProofContext.init thy;
     val (_, (gr, (_, idx_tab))) =
-      Nbe_Functions.change theory (fn thy => ensure_stmts (ProofContext.init thy) naming program o snd);
+      Nbe_Functions.change thy (ensure_stmts ctxt naming program o snd);
   in
     vs_t
-    |> eval_term (ProofContext.init theory) gr deps
-    |> term_of_univ theory program idx_tab
+    |> eval_term ctxt gr deps
+    |> term_of_univ thy program idx_tab
   end;
 
 (* evaluation with type reconstruction *)