# HG changeset patch
# User wenzelm
# Date 1368816105 -7200
# Node ID 2f970c7f722bc43b5f836d8fc6a64bebfa70951b
# Parent  387dc978422baa3f9e966d2880cf988f978b1d00
proper option quick_and_dirty;

diff -r 387dc978422b -r 2f970c7f722b NEWS
--- a/NEWS	Fri May 17 20:30:04 2013 +0200
+++ b/NEWS	Fri May 17 20:41:45 2013 +0200
@@ -6,6 +6,12 @@
 
 *** General ***
 
+* Uniform management of "quick_and_dirty" as system option (see also
+"isabelle options"), configuration option within the context (see also
+Config.get in Isabelle/ML), and attribute in Isabelle/Isar.  Minor
+INCOMPATIBILITY, need to use more official Isabelle means to access
+quick_and_dirty, instead of historical poking into mutable reference.
+
 * Sessions may be organized via 'chapter' specifications in the ROOT
 file, which determines a two-level hierarchy of browser info.  The old
 tree-like organization via implicit sub-session relation, with its
diff -r 387dc978422b -r 2f970c7f722b src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/IsarRef/Proof.thy	Fri May 17 20:41:45 2013 +0200
@@ -668,8 +668,8 @@
   
   \item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
   pretending to solve the pending claim without further ado.  This
-  only works in interactive development, or if the @{ML
-  quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
+  only works in interactive development, or if the @{attribute
+  quick_and_dirty} is enabled.  Facts emerging from fake
   proofs are not the real thing.  Internally, the derivation object is
   tainted by an oracle invocation, which may be inspected via the
   theorem status \cite{isabelle-implementation}.
diff -r 387dc978422b -r 2f970c7f722b src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/ProgProve/Isar.thy	Fri May 17 20:41:45 2013 +0200
@@ -2,7 +2,7 @@
 theory Isar
 imports LaTeXsugar
 begin
-ML{* quick_and_dirty := true *}
+declare [[quick_and_dirty]]
 (*>*)
 text{*
 Apply-scripts are unreadable and hard to maintain. The language of choice
diff -r 387dc978422b -r 2f970c7f722b src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri May 17 20:41:45 2013 +0200
@@ -168,7 +168,7 @@
       mk_comp_bd_cinfinite_tac (bd_cinfinite_of_bnf inner) (bd_cinfinite_of_bnf outer);
 
     val set_alt_thms =
-      if ! quick_and_dirty then
+      if Config.get lthy quick_and_dirty then
         []
       else
         map (fn goal =>
@@ -182,7 +182,7 @@
       mk_comp_map_cong0_tac set_alt_thms (map_cong0_of_bnf outer) (map map_cong0_of_bnf inners);
 
     val set_bd_tacs =
-      if ! quick_and_dirty then
+      if Config.get lthy quick_and_dirty then
         replicate ilive (K all_tac)
       else
         let
@@ -402,7 +402,7 @@
     fun map_cong0_tac {context = ctxt, prems = _} =
       rtac (map_cong0_of_bnf bnf) 1 THEN REPEAT_DETERM_N live (Goal.assume_rule_tac ctxt 1);
     val set_map_tacs =
-      if ! quick_and_dirty then
+      if Config.get lthy quick_and_dirty then
         replicate (n + live) (K all_tac)
       else
         replicate n (K empty_natural_tac) @
@@ -410,7 +410,7 @@
     fun bd_card_order_tac _ = rtac (bd_card_order_of_bnf bnf) 1;
     fun bd_cinfinite_tac _ = rtac (bd_cinfinite_of_bnf bnf) 1;
     val set_bd_tacs =
-      if ! quick_and_dirty then
+      if Config.get lthy quick_and_dirty then
         replicate (n + live) (K all_tac)
       else
         replicate n (K (mk_lift_set_bd_tac (bd_Card_order_of_bnf bnf))) @
diff -r 387dc978422b -r 2f970c7f722b src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Fri May 17 20:41:45 2013 +0200
@@ -132,7 +132,7 @@
         Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
     let val pth =
           (* If quick_and_dirty then run without proof generation as oracle*)
-             if !quick_and_dirty
+             if Config.get ctxt quick_and_dirty
              then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
              else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
     in 
diff -r 387dc978422b -r 2f970c7f722b src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Fri May 17 20:41:45 2013 +0200
@@ -158,7 +158,7 @@
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-e 'Unsynchronized.setmp Multithreading.max_threads 1 (Unsynchronized.setmp quick_and_dirty true use_thy) \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+  "-o quick_and_dirty -e 'Unsynchronized.setmp Multithreading.max_threads 1 use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
 if ($output_log) {
   my $outcome = ($result ? "failure" : "success");
diff -r 387dc978422b -r 2f970c7f722b src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Fri May 17 20:41:45 2013 +0200
@@ -850,7 +850,7 @@
 fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
    let
     val cpth = 
-       if !quick_and_dirty 
+       if Config.get ctxt quick_and_dirty
        then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
        else Conv.arg_conv (conv ctxt) p
     val p' = Thm.rhs_of cpth
diff -r 387dc978422b -r 2f970c7f722b src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri May 17 20:41:45 2013 +0200
@@ -116,7 +116,9 @@
 (** misc utilities **)
 
 fun message quiet_mode s = if quiet_mode then () else writeln s;
-fun clean_message quiet_mode s = if ! quick_and_dirty then () else message quiet_mode s;
+
+fun clean_message ctxt quiet_mode s =
+  if Config.get ctxt quick_and_dirty then () else message quiet_mode s;
 
 fun coind_prefix true = "co"
   | coind_prefix false = "";
@@ -361,7 +363,7 @@
 (* prove monotonicity *)
 
 fun prove_mono quiet_mode skip_mono predT fp_fun monos ctxt =
- (message (quiet_mode orelse skip_mono andalso ! quick_and_dirty)
+ (message (quiet_mode orelse skip_mono andalso Config.get ctxt quick_and_dirty)
     "  Proving monotonicity ...";
   (if skip_mono then Goal.prove_sorry else Goal.prove_future) ctxt
     [] []
@@ -379,7 +381,7 @@
 
 fun prove_intrs quiet_mode coind mono fp_def k intr_ts rec_preds_defs ctxt ctxt' =
   let
-    val _ = clean_message quiet_mode "  Proving the introduction rules ...";
+    val _ = clean_message ctxt quiet_mode "  Proving the introduction rules ...";
 
     val unfold = funpow k (fn th => th RS fun_cong)
       (mono RS (fp_def RS
@@ -404,7 +406,7 @@
 
 fun prove_elims quiet_mode cs params intr_ts intr_names unfold rec_preds_defs ctxt ctxt''' =
   let
-    val _ = clean_message quiet_mode "  Proving the elimination rules ...";
+    val _ = clean_message ctxt quiet_mode "  Proving the elimination rules ...";
 
     val ([pname], ctxt') = Variable.variant_fixes ["P"] ctxt;
     val P = HOLogic.mk_Trueprop (Free (pname, HOLogic.boolT));
@@ -453,7 +455,7 @@
 fun prove_eqs quiet_mode cs params intr_ts intrs
     (elims: (thm * bstring list * int) list) ctxt ctxt'' =  (* FIXME ctxt'' ?? *)
   let
-    val _ = clean_message quiet_mode "  Proving the simplification rules ...";
+    val _ = clean_message ctxt quiet_mode "  Proving the simplification rules ...";
 
     fun dest_intr r =
       (the (dest_predicate cs params (HOLogic.dest_Trueprop (Logic.strip_assums_concl r))),
@@ -640,7 +642,7 @@
 fun prove_indrule quiet_mode cs argTs bs xs rec_const params intr_ts mono
     fp_def rec_preds_defs ctxt ctxt''' =  (* FIXME ctxt''' ?? *)
   let
-    val _ = clean_message quiet_mode "  Proving the induction rule ...";
+    val _ = clean_message ctxt quiet_mode "  Proving the induction rule ...";
 
     (* predicates for induction rule *)
 
diff -r 387dc978422b -r 2f970c7f722b src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Fri May 17 20:41:45 2013 +0200
@@ -41,8 +41,8 @@
   dependent) configuration settings.  To replay SAT proofs in Isabelle, you
   must of course use a proof-producing SAT solver in the first place.
 
-  Proofs are replayed only if "!quick_and_dirty" is false.  If
-  "!quick_and_dirty" is true, the theorem (in case the SAT solver claims its
+  Proofs are replayed only if "quick_and_dirty" is false.  If
+  "quick_and_dirty" is true, the theorem (in case the SAT solver claims its
   negation to be unsatisfiable) is proved via an oracle.
 *)
 
@@ -351,7 +351,7 @@
               (Inttab.dest clause_table) ^ "\n" ^
             "empty clause: " ^ string_of_int empty_id)
         else ();
-        if !quick_and_dirty then
+        if Config.get ctxt quick_and_dirty then
           make_quick_and_dirty_thm ()
         else
           let
@@ -378,7 +378,7 @@
             Thm.implies_elim (Thm.implies_intr cnf_cterm raw_thm) clauses_thm
           end)
     | SatSolver.UNSATISFIABLE NONE =>
-        if !quick_and_dirty then
+        if Config.get ctxt quick_and_dirty then
          (warning "SAT solver claims the formula to be unsatisfiable, but did not provide a proof";
           make_quick_and_dirty_thm ())
         else
diff -r 387dc978422b -r 2f970c7f722b src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:41:45 2013 +0200
@@ -11,7 +11,7 @@
 (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
 (* ML {* sat.solver := "minisat_with_proofs"; *} *)
 ML {* sat.trace_sat := true; *}
-ML {* quick_and_dirty := true; *}
+declare [[quick_and_dirty]]
 
 lemma "True"
 by sat
@@ -78,7 +78,7 @@
 by sat
 
 ML {* sat.trace_sat := false; *}
-ML {* quick_and_dirty := false; *}
+declare [[quick_and_dirty = false]]
 
 method_setup rawsat = {*
   Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
@@ -522,8 +522,9 @@
 (* ML {*
 sat.solver := "zchaff_with_proofs";
 sat.trace_sat := false;
-quick_and_dirty := false;
-*} *)
+*}
+declare [[quick_and_dirty = false]]
+*)
 
 ML {*
 fun benchmark dimacsfile =
diff -r 387dc978422b -r 2f970c7f722b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri May 17 20:41:45 2013 +0200
@@ -553,7 +553,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Ast.trace_raw #>
+ (register_config quick_and_dirty_raw #>
+  register_config Ast.trace_raw #>
   register_config Ast.stats_raw #>
   register_config Printer.show_brackets_raw #>
   register_config Printer.show_sorts_raw #>
diff -r 387dc978422b -r 2f970c7f722b src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 17 20:41:45 2013 +0200
@@ -20,7 +20,7 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val cheating: bool -> method
+  val cheating: Proof.context -> bool -> method
   val intro: thm list -> method
   val elim: thm list -> method
   val unfold: thm list -> Proof.context -> method
@@ -127,8 +127,8 @@
 
 (* cheating *)
 
-fun cheating int = METHOD (fn _ => fn st =>
-  if int orelse ! quick_and_dirty then
+fun cheating ctxt int = METHOD (fn _ => fn st =>
+  if int orelse Config.get ctxt quick_and_dirty then
     ALLGOALS Skip_Proof.cheat_tac st
   else error "Cheating requires quick_and_dirty mode!");
 
@@ -296,7 +296,7 @@
 val default_text = Source (Args.src (("default", []), Position.none));
 val this_text = Basic (K this);
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
-fun sorry_text int = Basic (K (cheating int));
+fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
 
 fun finish_text (NONE, immed) = Basic (finish immed)
   | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];
diff -r 387dc978422b -r 2f970c7f722b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/ROOT.ML	Fri May 17 20:41:45 2013 +0200
@@ -6,9 +6,6 @@
   val is_official = false;
 end;
 
-(*if true then some tools will OMIT some proofs*)
-val quick_and_dirty = Unsynchronized.ref false;
-
 print_depth 10;
 
 
@@ -118,6 +115,9 @@
 use "context_position.ML";
 use "config.ML";
 
+val quick_and_dirty_raw = Config.declare_option "quick_and_dirty";
+val quick_and_dirty = Config.bool quick_and_dirty_raw;
+
 
 (* inner syntax *)
 
diff -r 387dc978422b -r 2f970c7f722b src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Tools/build.ML	Fri May 17 20:41:45 2013 +0200
@@ -114,7 +114,6 @@
     |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     |> Unsynchronized.setmp Future.ML_statistics true
     |> no_document options ? Present.no_document
-    |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     |> Unsynchronized.setmp Goal.skip_proofs (Options.bool options "skip_proofs")
     |> Unsynchronized.setmp Pretty.margin_default (Options.int options "pretty_margin")
     |> Unsynchronized.setmp Toplevel.timing (Options.bool options "timing");
diff -r 387dc978422b -r 2f970c7f722b src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Fri May 17 20:41:45 2013 +0200
@@ -131,9 +131,9 @@
 (* proof *)
 
 val _ =
-  ProofGeneral.preference_bool ProofGeneral.category_proof
+  ProofGeneral.preference_option ProofGeneral.category_proof
     (SOME "true")
-    quick_and_dirty
+    @{option quick_and_dirty}
     "quick-and-dirty"
     "Take a few short cuts";
 
diff -r 387dc978422b -r 2f970c7f722b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri May 17 20:30:04 2013 +0200
+++ b/src/Pure/goal.ML	Fri May 17 20:41:45 2013 +0200
@@ -337,7 +337,7 @@
   Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
 
 fun prove_sorry ctxt xs asms prop tac =
-  if ! quick_and_dirty then
+  if Config.get ctxt quick_and_dirty then
     prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
 
diff -r 387dc978422b -r 2f970c7f722b src/Tools/Code/lib/Tools/codegen
--- a/src/Tools/Code/lib/Tools/codegen	Fri May 17 20:30:04 2013 +0200
+++ b/src/Tools/Code/lib/Tools/codegen	Fri May 17 20:41:45 2013 +0200
@@ -55,9 +55,8 @@
   handle _ => exit 1;"
 
 ACTUAL_CMD="val thyname = \"$THYNAME\"; \
-  val _ = quick_and_dirty := $QUICK_AND_DIRTY; \
   val cmd_expr = \"$CODE_EXPR\"; \
   val ml_cmd = \"Code_Target.codegen_tool thyname cmd_expr\"; \
   $FORMAL_CMD"
 
-"$ISABELLE_PROCESS" -r -q -e "$ACTUAL_CMD" "$IMAGE" || exit 1
+"$ISABELLE_PROCESS" -r -q -o "quick_and_dirty=$QUICK_AND_DIRTY" -e "$ACTUAL_CMD" "$IMAGE" || exit 1