ignore code cache optionally

--- a/src/Pure/Isar/code.ML	Wed Sep 15 13:44:11 2010 +0200
+++ b/src/Pure/Isar/code.ML	Wed Sep 15 15:11:39 2010 +0200
@@ -89,16 +89,14 @@
 signature CODE_DATA =
 sig
   type T
-  val change: theory -> (T -> T) -> T
-  val change_yield: theory -> (T -> 'a * T) -> 'a * T
+  val change: theory option -> (T -> T) -> T
+  val change_yield: theory option -> (T -> 'a * T) -> 'a * T
 end;
 
 signature PRIVATE_CODE =
 sig
   include CODE
   val declare_data: Object.T -> serial
-  val change_data: serial * ('a -> Object.T) * (Object.T -> 'a)
-    -> theory -> ('a -> 'a) -> 'a
   val change_yield_data: serial * ('a -> Object.T) * (Object.T -> 'a)
     -> theory -> ('a -> 'b * 'a) -> 'b * 'a
 end;
@@ -310,8 +308,6 @@
       ((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 (f #> pair ()) |> snd;
-
 end; (*local*)
 
 
@@ -1277,8 +1273,10 @@
 
 val data_op = (kind, Data, dest);
 
-val change = Code.change_data data_op;
-fun change_yield thy = Code.change_yield_data data_op thy;
+fun change_yield (SOME thy) f = Code.change_yield_data data_op thy f
+  | change_yield NONE f = f Data.empty
+
+fun change some_thy f = snd (change_yield some_thy (pair () o f));
 
 end;
 

--- a/src/Tools/Code/code_thingol.ML	Wed Sep 15 13:44:11 2010 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 15 15:11:39 2010 +0200
@@ -832,15 +832,11 @@
   val empty = (empty_naming, Graph.empty);
 );
 
-fun cache_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)));
-
-fun transient_generation thy (algebra, eqngr) f name =
-  (NONE, (empty_naming, Graph.empty))
-  |> f thy algebra eqngr name
-  |-> (fn name => fn (_, naming_program) => (name, naming_program));
+fun invoke_generation ignore_cache thy (algebra, eqngr) f name =
+  Program.change_yield (if ignore_cache then NONE else SOME thy)
+    (fn naming_program => (NONE, naming_program)
+      |> f thy algebra eqngr name
+      |-> (fn name => fn (_, naming_program) => (name, naming_program)));
 
 
 (* program generation *)
@@ -853,10 +849,9 @@
       in (cs, (naming, Graph.subgraph (member (op =) cs_all) program)) end;
     fun generate_consts thy algebra eqngr =
       fold_map (ensure_const thy algebra eqngr permissive);
-    val invoke_generation = if permissive
-      then transient_generation else cache_generation
   in
-    invoke_generation thy (Code_Preproc.obtain thy cs []) generate_consts cs
+    invoke_generation (not permissive) thy (Code_Preproc.obtain false thy cs [])
+      generate_consts cs
     |-> project_consts
   end;
 
@@ -892,7 +887,7 @@
 fun base_evaluator thy evaluator algebra eqngr vs t =
   let
     val (((naming, program), (((vs', ty'), t'), deps)), _) =
-      cache_generation thy (algebra, eqngr) ensure_value t;
+      invoke_generation false thy (algebra, eqngr) ensure_value t;
     val vs'' = map (fn (v, _) => (v, (the o AList.lookup (op =) vs o prefix "'") v)) vs';
   in evaluator naming program ((vs'', (vs', ty')), t') deps end;
 
@@ -926,7 +921,7 @@
 
 fun code_depgr thy consts =
   let
-    val (_, eqngr) = Code_Preproc.obtain thy consts [];
+    val (_, eqngr) = Code_Preproc.obtain true thy consts [];
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.subgraph (member (op =) all_consts) eqngr end;