CRITICAL markup for critical poking with unsynchronized references;

--- a/src/HOL/HOL.thy	Wed Jan 26 20:51:09 2011 +0100
+++ b/src/HOL/HOL.thy	Thu Jan 27 16:24:29 2011 +0100
@@ -1958,7 +1958,7 @@
 subsubsection {* Evaluation and normalization by evaluation *}
 
 setup {*
-  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
+  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)  (* FIXME proper context!? *)
 *}
 
 ML {*

--- a/src/HOL/Tools/inductive_codegen.ML	Wed Jan 26 20:51:09 2011 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jan 27 16:24:29 2011 +0100
@@ -7,7 +7,7 @@
 signature INDUCTIVE_CODEGEN =
 sig
   val add : string option -> int option -> attribute
-  val test_fn : (int * int * int -> term list option) Unsynchronized.ref
+  val test_fn : (int * int * int -> term list option) Unsynchronized.ref  (* FIXME *)
   val test_term:
     Proof.context -> term -> int -> term list option * Quickcheck.report option
   val setup : theory -> theory
@@ -845,12 +845,12 @@
           Pretty.brk 1,
           Codegen.str "| NONE => NONE);"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
+    val test_fn' = NAMED_CRITICAL "codegen" (fn () =>
+     (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn));
     val values = Config.get ctxt random_values;
     val bound = Config.get ctxt depth_bound;
     val start = Config.get ctxt depth_start;
     val offset = Config.get ctxt size_offset;
-    val test_fn' = !test_fn;
     fun test k = (deepen bound (fn i =>
       (Output.urgent_message ("Search depth: " ^ string_of_int i);
        test_fn' (i, values, k+offset))) start, NONE);

--- a/src/Pure/codegen.ML	Wed Jan 26 20:51:09 2011 +0100
+++ b/src/Pure/codegen.ML	Thu Jan 27 16:24:29 2011 +0100
@@ -75,9 +75,9 @@
   val mk_type: bool -> typ -> Pretty.T
   val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
   val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
-  val test_fn: (int -> term list option) Unsynchronized.ref
+  val test_fn: (int -> term list option) Unsynchronized.ref  (* FIXME *)
   val test_term: Proof.context -> term -> int -> term list option
-  val eval_result: (unit -> term) Unsynchronized.ref
+  val eval_result: (unit -> term) Unsynchronized.ref  (* FIXME *)
   val eval_term: theory -> term -> term
   val evaluation_conv: cterm -> thm
   val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list
@@ -894,8 +894,9 @@
                 Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
           str ");"]) ^
       "\n\nend;\n";
-    val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
-  in (fn size => (! test_fn size)) end;
+    val test_fn' = NAMED_CRITICAL "codegen" (fn () =>
+      (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! test_fn));
+  in test_fn' end;
 
 
 
@@ -905,7 +906,7 @@
 
 fun eval_term thy t =
   let
-    val ctxt = ProofContext.init_global thy;
+    val ctxt = ProofContext.init_global thy;  (* FIXME *)
     val e =
       let
         val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
@@ -924,9 +925,10 @@
                 [str "(result ())"],
               str ");"]) ^
           "\n\nend;\n";
-        val _ = NAMED_CRITICAL "codegen" (fn () =>   (* FIXME ??? *)
-          ML_Context.eval_text_in (SOME ctxt) false Position.none s);
-      in !eval_result end;
+      in
+        NAMED_CRITICAL "codegen" (fn () =>
+         (ML_Context.eval_text_in (SOME ctxt) false Position.none s; ! eval_result))
+      end
   in e () end;
 
 val (_, evaluation_conv) = Context.>>> (Context.map_theory_result