modernized diagnostic options

--- a/src/Tools/Code/code_runtime.ML	Sun Jun 29 18:30:24 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Sun Jun 29 18:02:18 2014 +0200
@@ -32,7 +32,7 @@
     -> string option -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
-  val trace: bool Unsynchronized.ref
+  val trace: bool Config.T
   val polyml_as_definition: (binding * typ) list -> Path.T list -> theory -> theory
 end;
 
@@ -65,10 +65,10 @@
   #> fold (Code_Target.add_reserved target) ["oo", "ooo", "oooo", "upto", "downto", "orf", "andf"]);
        (*avoid further pervasive infix names*)
 
-val trace = Unsynchronized.ref false;
+val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
 
-fun exec verbose code =
-  (if ! trace then tracing code else ();
+fun exec ctxt verbose code =
+  (if Config.get ctxt trace then tracing code else ();
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
@@ -78,7 +78,7 @@
       ^ " (fn () => " ^ value ^ ")) (ML_Context.the_generic_context ())))");
     val ctxt' = ctxt
       |> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
-      |> Context.proof_map (exec false code);
+      |> Context.proof_map (exec ctxt false code);
   in get ctxt' () end;
 
 
@@ -112,7 +112,7 @@
 fun dynamic_value_exn cookie ctxt some_target postproc t args =
   let
     val _ = reject_vars ctxt t;
-    val _ = if ! trace
+    val _ = if Config.get ctxt trace
       then tracing ("Evaluation of term " ^ quote (Syntax.string_of_term ctxt t))
       else ()
     fun evaluator program _ vs_ty_t deps =
@@ -313,7 +313,7 @@
 fun process_reflection (code, (tyco_map, (constr_map, const_map))) module_name NONE thy =
       thy
       |> Code_Target.add_reserved target module_name
-      |> Context.theory_map (exec true code)
+      |> Context.theory_map (exec (Proof_Context.init_global thy (*FIXME*)) true code)
       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
       |> fold (add_eval_const o apsnd Code_Printer.str) const_map

--- a/src/Tools/nbe.ML	Sun Jun 29 18:30:24 2014 +0200
+++ b/src/Tools/nbe.ML	Sun Jun 29 18:02:18 2014 +0200
@@ -22,7 +22,7 @@
   val same: Univ * Univ -> bool
 
   val put_result: (unit -> Univ list -> Univ list) -> Proof.context -> Proof.context
-  val trace: bool Unsynchronized.ref
+  val trace: bool Config.T
 
   val add_const_alias: thm -> theory -> theory
 end;
@@ -32,8 +32,8 @@
 
 (* generic non-sense *)
 
-val trace = Unsynchronized.ref false;
-fun traced f x = if !trace then (tracing (f x); x) else x;
+val trace = Attrib.setup_config_bool @{binding "nbe_trace"} (K false);
+fun traced ctxt f x = if Config.get ctxt trace then (tracing (f x); x) else x;
 
 
 (** certificates and oracle for "trivial type classes" **)
@@ -263,9 +263,10 @@
 fun nbe_apps t [] = t
   | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)];
 fun nbe_apps_local idx_of i c ts = nbe_fun idx_of i c `$` ml_list (rev ts);
-fun nbe_apps_constr idx_of c ts =
+fun nbe_apps_constr ctxt idx_of c ts =
   let
-    val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
+    val c' = if Config.get ctxt trace
+      then string_of_int (idx_of c) ^ " (*" ^ Code_Symbol.default_base c ^ "*)"
       else string_of_int (idx_of c);
   in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
 
@@ -282,7 +283,7 @@
 
 (* code generation *)
 
-fun assemble_eqnss idx_of deps eqnss =
+fun assemble_eqnss ctxt idx_of deps eqnss =
   let
     fun prep_eqns (c, (vs, eqns)) =
       let
@@ -301,7 +302,7 @@
             end else nbe_apps (nbe_abss num_args (nbe_fun idx_of 0 sym)) ts'
         | NONE => if member (op =) deps sym
             then nbe_apps (nbe_fun idx_of 0 sym) ts'
-            else nbe_apps_constr idx_of sym ts'
+            else nbe_apps_constr ctxt idx_of sym ts'
       end
     and assemble_classrels classrels =
       fold_rev (fn classrel => assemble_constapp (Class_Relation classrel) [] o single) classrels
@@ -358,7 +359,8 @@
         val match_cont = if Code_Symbol.is_value sym then NONE
           else SOME (nbe_apps_local idx_of (i + 1) sym (dicts @ default_args));
         val assemble_arg = assemble_iterm
-          (fn sym' => fn dss => fn ts => nbe_apps_constr idx_of sym' ((maps o map) (K "_") dss @ ts)) NONE;
+          (fn sym' => fn dss => fn ts => nbe_apps_constr ctxt idx_of sym' ((maps o map) (K "_")
+            dss @ ts)) NONE;
         val assemble_rhs = assemble_iterm assemble_constapp match_cont;
         val (samepairs, args') = subst_nonlin_vars args;
         val s_args = map assemble_arg args';
@@ -379,7 +381,7 @@
         val eqns' = map_index (assemble_eqn sym dicts default_args) eqns
           @ (if Code_Symbol.is_value sym then [] else [(nbe_fun idx_of (length eqns) sym,
             [([ml_list (rev (dicts @ default_args))],
-              nbe_apps_constr idx_of sym (dicts @ default_args))])]);
+              nbe_apps_constr ctxt idx_of sym (dicts @ default_args))])]);
       in (eqns', nbe_abss num_args (nbe_fun idx_of 0 sym)) end;
 
     val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
@@ -398,11 +400,11 @@
           |> map (fn dep => (dep, snd (Code_Symbol.Graph.get_node nbe_program dep)))
           |> AList.lookup (op =)
           |> (fn f => the o f);
-        val s = assemble_eqnss idx_of deps eqnss;
+        val s = assemble_eqnss ctxt idx_of deps eqnss;
         val cs = map fst eqnss;
       in
         s
-        |> traced (fn s => "\n--- code to be evaluated:\n" ^ s)
+        |> traced ctxt (fn s => "\n--- code to be evaluated:\n" ^ s)
         |> pair ""
         |> Code_Runtime.value ctxt univs_cookie
         |> (fn f => f deps_vals)
@@ -549,11 +551,11 @@
   in
     compile_term ctxt nbe_program deps (vs, t)
     |> term_of_univ ctxt idx_tab
-    |> traced (fn t => "Normalized:\n" ^ string_of_term t)
+    |> traced ctxt (fn t => "Normalized:\n" ^ string_of_term t)
     |> type_infer
-    |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
+    |> traced ctxt (fn t => "Types inferred:\n" ^ string_of_term t)
     |> check_tvars
-    |> traced (fn _ => "---\n")
+    |> traced ctxt (fn _ => "---\n")
   end;