indicate CRITICAL nature of various setmp combinators;
authorwenzelm
Sat Oct 17 15:57:51 2009 +0200 (2009-10-17)
changeset 329665b21661fe618
parent 32965 ecb746bca732
child 32967 1df87354c308
indicate CRITICAL nature of various setmp combinators;
doc-src/IsarImplementation/Thy/ML.thy
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/fundef_common.ML
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/typedef.ML
src/Pure/General/output.ML
src/Pure/General/pretty.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/Isar/method.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/skip_proof.ML
src/Pure/ML/ml_context.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/printer.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/goal_display.ML
src/Pure/library.ML
src/Pure/old_goals.ML
src/Pure/theory.ML
src/Tools/Code/code_target.ML
src/Tools/auto_solve.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
     1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Sat Oct 17 15:55:57 2009 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Sat Oct 17 15:57:51 2009 +0200
     1.3 @@ -229,7 +229,7 @@
     1.4    view being presented to the user.
     1.5  
     1.6    Occasionally, such global process flags are treated like implicit
     1.7 -  arguments to certain operations, by using the @{ML setmp} combinator
     1.8 +  arguments to certain operations, by using the @{ML setmp_CRITICAL} combinator
     1.9    for safe temporary assignment.  Its traditional purpose was to
    1.10    ensure proper recovery of the original value when exceptions are
    1.11    raised in the body, now the functionality is extended to enter the
    1.12 @@ -237,7 +237,7 @@
    1.13    parallelism).
    1.14  
    1.15    Note that recovery of plain value passing semantics via @{ML
    1.16 -  setmp}~@{text "ref value"} assumes that this @{text "ref"} is
    1.17 +  setmp_CRITICAL}~@{text "ref value"} assumes that this @{text "ref"} is
    1.18    exclusively manipulated within the critical section.  In particular,
    1.19    any persistent global assignment of @{text "ref := value"} needs to
    1.20    be marked critical as well, to prevent intruding another threads
    1.21 @@ -258,7 +258,7 @@
    1.22    \begin{mldecls}
    1.23    @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
    1.24    @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
    1.25 -  @{index_ML setmp: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
    1.26 +  @{index_ML setmp_CRITICAL: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
    1.27    \end{mldecls}
    1.28  
    1.29    \begin{description}
    1.30 @@ -272,7 +272,7 @@
    1.31    \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
    1.32    name argument.
    1.33  
    1.34 -  \item @{ML setmp}~@{text "ref value f x"} evaluates @{text "f x"}
    1.35 +  \item @{ML setmp_CRITICAL}~@{text "ref value f x"} evaluates @{text "f x"}
    1.36    while staying within the critical section and having @{text "ref :=
    1.37    value"} assigned temporarily.  This recovers a value-passing
    1.38    semantics involving global references, regardless of exceptions or
     2.1 --- a/src/HOL/Import/proof_kernel.ML	Sat Oct 17 15:55:57 2009 +0200
     2.2 +++ b/src/HOL/Import/proof_kernel.ML	Sat Oct 17 15:57:51 2009 +0200
     2.3 @@ -201,10 +201,10 @@
     2.4      in
     2.5          quote (
     2.6          PrintMode.setmp [] (
     2.7 -        Library.setmp show_brackets false (
     2.8 -        Library.setmp show_all_types true (
     2.9 -        Library.setmp Syntax.ambiguity_is_error false (
    2.10 -        Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
    2.11 +        setmp_CRITICAL show_brackets false (
    2.12 +        setmp_CRITICAL show_all_types true (
    2.13 +        setmp_CRITICAL Syntax.ambiguity_is_error false (
    2.14 +        setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
    2.15          ct)
    2.16      end
    2.17  
    2.18 @@ -219,15 +219,15 @@
    2.19          val ct  = (cterm_of thy (HOLogic.dest_Trueprop t)
    2.20                     handle TERM _ => ct)
    2.21          fun match u = t aconv u
    2.22 -        fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
    2.23 -          | G 1 = Library.setmp show_brackets true (G 0)
    2.24 -          | G 2 = Library.setmp show_all_types true (G 0)
    2.25 -          | G 3 = Library.setmp show_brackets true (G 2)
    2.26 +        fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
    2.27 +          | G 1 = setmp_CRITICAL show_brackets true (G 0)
    2.28 +          | G 2 = setmp_CRITICAL show_all_types true (G 0)
    2.29 +          | G 3 = setmp_CRITICAL show_brackets true (G 2)
    2.30            | G _ = raise SMART_STRING
    2.31          fun F n =
    2.32              let
    2.33                  val str =
    2.34 -                  Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
    2.35 +                  setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
    2.36                  val u = Syntax.parse_term ctxt str
    2.37                    |> TypeInfer.constrain T |> Syntax.check_term ctxt
    2.38              in
    2.39 @@ -239,7 +239,7 @@
    2.40                | SMART_STRING =>
    2.41                    error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
    2.42      in
    2.43 -      PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
    2.44 +      PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
    2.45      end
    2.46      handle ERROR mesg => simple_smart_string_of_cterm ct
    2.47  
    2.48 @@ -2124,7 +2124,7 @@
    2.49                                  else "(" ^ commas tnames ^ ") "
    2.50              val proc_prop = if null tnames
    2.51                              then smart_string_of_cterm
    2.52 -                            else Library.setmp show_all_types true smart_string_of_cterm
    2.53 +                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
    2.54              val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
    2.55                                   ^ (string_of_mixfix tsyn) ^ "\n  by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
    2.56  
    2.57 @@ -2219,7 +2219,7 @@
    2.58                                  else "(" ^ commas tnames ^ ") "
    2.59              val proc_prop = if null tnames
    2.60                              then smart_string_of_cterm
    2.61 -                            else Library.setmp show_all_types true smart_string_of_cterm
    2.62 +                            else setmp_CRITICAL show_all_types true smart_string_of_cterm
    2.63              val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
    2.64                " = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
    2.65                (string_of_mixfix tsyn) ^ " morphisms "^
     3.1 --- a/src/HOL/Import/replay.ML	Sat Oct 17 15:55:57 2009 +0200
     3.2 +++ b/src/HOL/Import/replay.ML	Sat Oct 17 15:57:51 2009 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4  
     3.5  fun replay_chached_thm int_thms thyname thmname =
     3.6      let
     3.7 -        fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
     3.8 +        fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
     3.9          fun err msg = raise ERR "replay_cached_thm" msg
    3.10          val _ = writeln ("Replaying (from cache) "^thmname^" ...")
    3.11          fun rps [] thy = thy
     4.1 --- a/src/HOL/Statespace/state_space.ML	Sat Oct 17 15:55:57 2009 +0200
     4.2 +++ b/src/HOL/Statespace/state_space.ML	Sat Oct 17 15:57:51 2009 +0200
     4.3 @@ -297,7 +297,7 @@
     4.4  
     4.5            val tt' = tt |> fold upd all_names;
     4.6            val activate_simproc =
     4.7 -              Output.no_warnings
     4.8 +              Output.no_warnings_CRITICAL
     4.9                 (Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
    4.10            val ctxt' =
    4.11                ctxt
    4.12 @@ -444,7 +444,7 @@
    4.13        in Context.mapping I upd_prf ctxt end;
    4.14  
    4.15     fun string_of_typ T =
    4.16 -      setmp show_sorts true
    4.17 +      setmp_CRITICAL show_sorts true
    4.18         (PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
    4.19     val fixestate = (case state_type of
    4.20           NONE => []
     5.1 --- a/src/HOL/Tools/Function/fundef_common.ML	Sat Oct 17 15:55:57 2009 +0200
     5.2 +++ b/src/HOL/Tools/Function/fundef_common.ML	Sat Oct 17 15:57:51 2009 +0200
     5.3 @@ -267,7 +267,7 @@
     5.4            Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
     5.5            orelse error (cat_lines 
     5.6            ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
     5.7 -           setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
     5.8 +           setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
     5.9  
    5.10        val _ = map check_sorts fixes
    5.11      in
     6.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 15:55:57 2009 +0200
     6.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 15:57:51 2009 +0200
     6.3 @@ -108,7 +108,7 @@
     6.4        in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
     6.5      val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     6.6      val t' = Pattern.rewrite_term thy rewr [] t
     6.7 -    val tac = setmp quick_and_dirty true (SkipProof.cheat_tac thy)
     6.8 +    val tac = setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy)
     6.9      val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
    6.10      val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
    6.11    in
     7.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 15:55:57 2009 +0200
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 15:57:51 2009 +0200
     7.3 @@ -56,7 +56,7 @@
     7.4      val ((_, intros), ctxt') = Variable.import true intros ctxt
     7.5      val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
     7.6        (flatten constname) (map prop_of intros) ([], thy)
     7.7 -    val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
     7.8 +    val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
     7.9      val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
    7.10        |> Variable.export ctxt' ctxt
    7.11    in
     8.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 15:55:57 2009 +0200
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 15:57:51 2009 +0200
     8.3 @@ -58,7 +58,7 @@
     8.4      val t = Logic.list_implies
     8.5        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
     8.6         HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
     8.7 -    val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
     8.8 +    val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
     8.9      val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
    8.10      val _ = tracing (Display.string_of_thm ctxt' intro)
    8.11      val thy'' = thy'
     9.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 15:55:57 2009 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 15:57:51 2009 +0200
     9.3 @@ -661,7 +661,7 @@
     9.4      val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
     9.5      val nparams = guess_nparams T
     9.6      val pre_elim = 
     9.7 -      (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
     9.8 +      (Drule.standard o (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)))
     9.9        (mk_casesrule (ProofContext.init thy) nparams pre_intros)
    9.10    in register_predicate (pre_intros, pre_elim, nparams) thy end
    9.11  
    9.12 @@ -2077,12 +2077,12 @@
    9.13        (if !do_proofs then
    9.14          (fn _ =>
    9.15          rtac @{thm pred_iffI} 1
    9.16 -				THEN print_tac "after pred_iffI"
    9.17 +        THEN print_tac "after pred_iffI"
    9.18          THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
    9.19          THEN print_tac "proved one direction"
    9.20          THEN prove_other_direction thy modes pred mode moded_clauses
    9.21          THEN print_tac "proved other direction")
    9.22 -      else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
    9.23 +      else (fn _ => setmp_CRITICAL quick_and_dirty true SkipProof.cheat_tac thy))
    9.24    end;
    9.25  
    9.26  (* composition of mode inference, definition, compilation and proof *)
    9.27 @@ -2110,7 +2110,8 @@
    9.28      (join_preds_modes moded_clauses compiled_terms)
    9.29  
    9.30  fun prove_by_skip thy _ _ _ _ compiled_terms =
    9.31 -  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
    9.32 +  map_preds_modes (fn pred => fn mode => fn t =>
    9.33 +      Drule.standard (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy) t))
    9.34      compiled_terms
    9.35      
    9.36  fun prepare_intrs thy prednames =
    10.1 --- a/src/HOL/Tools/res_reconstruct.ML	Sat Oct 17 15:55:57 2009 +0200
    10.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Sat Oct 17 15:57:51 2009 +0200
    10.3 @@ -354,7 +354,7 @@
    10.4              "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
    10.5        fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
    10.6          | dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
    10.7 -  in setmp show_sorts (Config.get ctxt recon_sorts) dolines end;
    10.8 +  in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
    10.9  
   10.10  fun notequal t (_,t',_) = not (t aconv t');
   10.11  
    11.1 --- a/src/HOL/Tools/typedef.ML	Sat Oct 17 15:55:57 2009 +0200
    11.2 +++ b/src/HOL/Tools/typedef.ML	Sat Oct 17 15:57:51 2009 +0200
    11.3 @@ -200,7 +200,7 @@
    11.4      (*test theory errors now!*)
    11.5      val test_thy = Theory.copy thy;
    11.6      val _ = test_thy
    11.7 -      |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
    11.8 +      |> typedef_result (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm test_thy) goal);
    11.9  
   11.10    in (set, goal, goal_pat, typedef_result) end
   11.11    handle ERROR msg =>
    12.1 --- a/src/Pure/General/output.ML	Sat Oct 17 15:55:57 2009 +0200
    12.2 +++ b/src/Pure/General/output.ML	Sat Oct 17 15:57:51 2009 +0200
    12.3 @@ -44,7 +44,7 @@
    12.4    val prompt: string -> unit
    12.5    val status: string -> unit
    12.6    val debugging: bool Unsynchronized.ref
    12.7 -  val no_warnings: ('a -> 'b) -> 'a -> 'b
    12.8 +  val no_warnings_CRITICAL: ('a -> 'b) -> 'a -> 'b
    12.9    val debug: (unit -> string) -> unit
   12.10  end;
   12.11  
   12.12 @@ -112,7 +112,7 @@
   12.13  fun legacy_feature s =
   12.14    (if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
   12.15  
   12.16 -fun no_warnings f = setmp warning_fn (K ()) f;
   12.17 +fun no_warnings_CRITICAL f = setmp_CRITICAL warning_fn (K ()) f;
   12.18  
   12.19  val debugging = Unsynchronized.ref false;
   12.20  fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
    13.1 --- a/src/Pure/General/pretty.ML	Sat Oct 17 15:55:57 2009 +0200
    13.2 +++ b/src/Pure/General/pretty.ML	Sat Oct 17 15:57:51 2009 +0200
    13.3 @@ -53,7 +53,7 @@
    13.4    val indent: int -> T -> T
    13.5    val unbreakable: T -> T
    13.6    val setmargin: int -> unit
    13.7 -  val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
    13.8 +  val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
    13.9    val setdepth: int -> unit
   13.10    val to_ML: T -> ML_Pretty.pretty
   13.11    val from_ML: ML_Pretty.pretty -> T
   13.12 @@ -188,7 +188,7 @@
   13.13  
   13.14  val margin_info = Unsynchronized.ref (make_margin_info 76);
   13.15  fun setmargin m = margin_info := make_margin_info m;
   13.16 -fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
   13.17 +fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
   13.18  
   13.19  
   13.20  (* depth limitation *)
    14.1 --- a/src/Pure/Isar/class_target.ML	Sat Oct 17 15:55:57 2009 +0200
    14.2 +++ b/src/Pure/Isar/class_target.ML	Sat Oct 17 15:57:51 2009 +0200
    14.3 @@ -177,7 +177,7 @@
    14.4          val Ss = Sorts.mg_domain algebra tyco [class];
    14.5        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    14.6      fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
    14.7 -      ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
    14.8 +      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
    14.9      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   14.10        (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   14.11        (SOME o Pretty.block) [Pretty.str "supersort: ",
    15.1 --- a/src/Pure/Isar/code.ML	Sat Oct 17 15:55:57 2009 +0200
    15.2 +++ b/src/Pure/Isar/code.ML	Sat Oct 17 15:57:51 2009 +0200
    15.3 @@ -94,7 +94,7 @@
    15.4  
    15.5  (* printing *)
    15.6  
    15.7 -fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
    15.8 +fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
    15.9  
   15.10  fun string_of_const thy c = case AxClass.inst_of_param thy c
   15.11   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
    16.1 --- a/src/Pure/Isar/method.ML	Sat Oct 17 15:55:57 2009 +0200
    16.2 +++ b/src/Pure/Isar/method.ML	Sat Oct 17 15:57:51 2009 +0200
    16.3 @@ -151,7 +151,7 @@
    16.4  
    16.5  (* cheating *)
    16.6  
    16.7 -fun cheating int ctxt = METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
    16.8 +fun cheating int ctxt = METHOD (K (setmp_CRITICAL quick_and_dirty (int orelse ! quick_and_dirty)
    16.9      (SkipProof.cheat_tac (ProofContext.theory_of ctxt))));
   16.10  
   16.11  
    17.1 --- a/src/Pure/Isar/obtain.ML	Sat Oct 17 15:55:57 2009 +0200
    17.2 +++ b/src/Pure/Isar/obtain.ML	Sat Oct 17 15:57:51 2009 +0200
    17.3 @@ -215,7 +215,7 @@
    17.4      val thy = ProofContext.theory_of ctxt;
    17.5      val certT = Thm.ctyp_of thy;
    17.6      val cert = Thm.cterm_of thy;
    17.7 -    val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
    17.8 +    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
    17.9  
   17.10      fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
   17.11  
    18.1 --- a/src/Pure/Isar/proof_context.ML	Sat Oct 17 15:55:57 2009 +0200
    18.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Oct 17 15:57:51 2009 +0200
    18.3 @@ -366,7 +366,7 @@
    18.4        (case try Name.dest_skolem x of
    18.5          NONE => Pretty.mark Markup.var (Pretty.str s)
    18.6        | SOME x' => Pretty.mark Markup.skolem
    18.7 -          (Pretty.str (setmp show_question_marks true Term.string_of_vname (x', i))))
    18.8 +          (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
    18.9    | NONE => Pretty.mark Markup.var (Pretty.str s));
   18.10  
   18.11  fun class_markup _ c =    (* FIXME authentic name *)
   18.12 @@ -1213,7 +1213,7 @@
   18.13  val verbose = Unsynchronized.ref false;
   18.14  fun verb f x = if ! verbose then f (x ()) else [];
   18.15  
   18.16 -fun setmp_verbose f x = Library.setmp verbose true f x;
   18.17 +fun setmp_verbose f x = setmp_CRITICAL verbose true f x;
   18.18  
   18.19  
   18.20  (* local syntax *)
    19.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:55:57 2009 +0200
    19.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 15:57:51 2009 +0200
    19.3 @@ -36,7 +36,7 @@
    19.4    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
    19.5      (fn args => fn st =>
    19.6        if ! quick_and_dirty
    19.7 -      then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    19.8 +      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
    19.9        else tac args st);
   19.10  
   19.11  fun prove_global thy xs asms prop tac =
    20.1 --- a/src/Pure/ML/ml_context.ML	Sat Oct 17 15:55:57 2009 +0200
    20.2 +++ b/src/Pure/ML/ml_context.ML	Sat Oct 17 15:57:51 2009 +0200
    20.3 @@ -64,7 +64,7 @@
    20.4        if name = "" then ()
    20.5        else if not (ML_Syntax.is_identifier name) then
    20.6          error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
    20.7 -      else setmp stored_thms ths' (fn () =>
    20.8 +      else setmp_CRITICAL stored_thms ths' (fn () =>
    20.9          ML_Compiler.eval true Position.none
   20.10            (ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
   20.11    in () end;
    21.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Oct 17 15:55:57 2009 +0200
    21.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Oct 17 15:57:51 2009 +0200
    21.3 @@ -78,7 +78,7 @@
    21.4  
    21.5  (* preferences of Pure *)
    21.6  
    21.7 -val proof_pref = setmp Proofterm.proofs 1 (fn () =>
    21.8 +val proof_pref = setmp_CRITICAL Proofterm.proofs 1 (fn () =>
    21.9    let
   21.10      fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
   21.11      fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   21.12 @@ -167,7 +167,7 @@
   21.13    thm_deps_pref];
   21.14  
   21.15  val proof_preferences =
   21.16 - [setmp quick_and_dirty true (fn () =>
   21.17 + [setmp_CRITICAL quick_and_dirty true (fn () =>
   21.18      bool_pref quick_and_dirty
   21.19        "quick-and-dirty"
   21.20        "Take a few short cuts") (),
    22.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 17 15:55:57 2009 +0200
    22.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Oct 17 15:57:51 2009 +0200
    22.3 @@ -231,7 +231,7 @@
    22.4  fun init false = panic "No Proof General interface support for Isabelle/classic mode."
    22.5    | init true =
    22.6        (! initialized orelse
    22.7 -        (Output.no_warnings init_outer_syntax ();
    22.8 +        (Output.no_warnings_CRITICAL init_outer_syntax ();
    22.9            Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
   22.10            Output.add_mode proof_generalN Output.default_output Output.default_escape;
   22.11            Markup.add_mode proof_generalN YXML.output_markup;
    23.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 17 15:55:57 2009 +0200
    23.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Oct 17 15:57:51 2009 +0200
    23.3 @@ -807,7 +807,8 @@
    23.4        val filepath = PgipTypes.path_of_pgipurl url
    23.5        val filedir = Path.dir filepath
    23.6        val thy_name = Path.implode o #1 o Path.split_ext o Path.base
    23.7 -      val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
    23.8 +      val openfile_retract = Output.no_warnings_CRITICAL
    23.9 +        (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
   23.10    in
   23.11        case !currently_open_file of
   23.12            SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   23.13 @@ -1030,7 +1031,7 @@
   23.14           Output.add_mode proof_generalN Output.default_output Output.default_escape;
   23.15           Markup.add_mode proof_generalN YXML.output_markup;
   23.16           setup_messages ();
   23.17 -         Output.no_warnings init_outer_syntax ();
   23.18 +         Output.no_warnings_CRITICAL init_outer_syntax ();
   23.19           setup_thy_loader ();
   23.20           setup_present_hook ();
   23.21           init_pgip_session_id ();
   23.22 @@ -1057,7 +1058,7 @@
   23.23     This works for preferences but not generally guaranteed
   23.24     because we haven't done full setup here (e.g., no pgml mode)  *)
   23.25  fun process_pgip str =
   23.26 -     setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
   23.27 +     setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
   23.28  
   23.29  end
   23.30  
    24.1 --- a/src/Pure/Syntax/printer.ML	Sat Oct 17 15:55:57 2009 +0200
    24.2 +++ b/src/Pure/Syntax/printer.ML	Sat Oct 17 15:57:51 2009 +0200
    24.3 @@ -48,7 +48,7 @@
    24.4  val show_no_free_types = Unsynchronized.ref false;
    24.5  val show_all_types = Unsynchronized.ref false;
    24.6  
    24.7 -fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
    24.8 +fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
    24.9    Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
   24.10  
   24.11  
    25.1 --- a/src/Pure/Thy/thy_load.ML	Sat Oct 17 15:55:57 2009 +0200
    25.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Oct 17 15:57:51 2009 +0200
    25.3 @@ -50,7 +50,7 @@
    25.4  fun reset_path () = load_path := [Path.current];
    25.5  
    25.6  fun with_paths ss f x =
    25.7 -  CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x);
    25.8 +  CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
    25.9  fun with_path s f x = with_paths [s] f x;
   25.10  
   25.11  fun search_path dir path =
    26.1 --- a/src/Pure/Thy/thy_output.ML	Sat Oct 17 15:55:57 2009 +0200
    26.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Oct 17 15:57:51 2009 +0200
    26.3 @@ -154,7 +154,7 @@
    26.4            let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
    26.5              options opts (fn () => command src state) ();  (*preview errors!*)
    26.6              PrintMode.with_modes (! modes @ Latex.modes)
    26.7 -              (Output.no_warnings (options opts (fn () => command src state))) ()
    26.8 +              (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
    26.9            end
   26.10        | expand (Antiquote.Open _) = ""
   26.11        | expand (Antiquote.Close _) = "";
   26.12 @@ -416,22 +416,22 @@
   26.13  (* options *)
   26.14  
   26.15  val _ = add_options
   26.16 - [("show_types", Library.setmp Syntax.show_types o boolean),
   26.17 -  ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
   26.18 -  ("show_structs", Library.setmp show_structs o boolean),
   26.19 -  ("show_question_marks", Library.setmp show_question_marks o boolean),
   26.20 -  ("long_names", Library.setmp NameSpace.long_names o boolean),
   26.21 -  ("short_names", Library.setmp NameSpace.short_names o boolean),
   26.22 -  ("unique_names", Library.setmp NameSpace.unique_names o boolean),
   26.23 -  ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
   26.24 -  ("display", Library.setmp display o boolean),
   26.25 -  ("break", Library.setmp break o boolean),
   26.26 -  ("quotes", Library.setmp quotes o boolean),
   26.27 + [("show_types", setmp_CRITICAL Syntax.show_types o boolean),
   26.28 +  ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
   26.29 +  ("show_structs", setmp_CRITICAL show_structs o boolean),
   26.30 +  ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
   26.31 +  ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
   26.32 +  ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
   26.33 +  ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
   26.34 +  ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
   26.35 +  ("display", setmp_CRITICAL display o boolean),
   26.36 +  ("break", setmp_CRITICAL break o boolean),
   26.37 +  ("quotes", setmp_CRITICAL quotes o boolean),
   26.38    ("mode", fn s => fn f => PrintMode.with_modes [s] f),
   26.39 -  ("margin", Pretty.setmp_margin o integer),
   26.40 -  ("indent", Library.setmp indent o integer),
   26.41 -  ("source", Library.setmp source o boolean),
   26.42 -  ("goals_limit", Library.setmp goals_limit o integer)];
   26.43 +  ("margin", Pretty.setmp_margin_CRITICAL o integer),
   26.44 +  ("indent", setmp_CRITICAL indent o integer),
   26.45 +  ("source", setmp_CRITICAL source o boolean),
   26.46 +  ("goals_limit", setmp_CRITICAL goals_limit o integer)];
   26.47  
   26.48  
   26.49  (* basic pretty printing *)
    27.1 --- a/src/Pure/axclass.ML	Sat Oct 17 15:55:57 2009 +0200
    27.2 +++ b/src/Pure/axclass.ML	Sat Oct 17 15:57:51 2009 +0200
    27.3 @@ -438,7 +438,7 @@
    27.4      fun check_constraint (a, S) =
    27.5        if Sign.subsort thy (super, S) then ()
    27.6        else error ("Sort constraint of type variable " ^
    27.7 -        setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
    27.8 +        setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
    27.9          " needs to be weaker than " ^ Pretty.string_of_sort pp super);
   27.10  
   27.11  
    28.1 --- a/src/Pure/codegen.ML	Sat Oct 17 15:55:57 2009 +0200
    28.2 +++ b/src/Pure/codegen.ML	Sat Oct 17 15:57:51 2009 +0200
    28.3 @@ -111,7 +111,7 @@
    28.4  
    28.5  fun string_of p = (Pretty.string_of |>
    28.6    PrintMode.setmp [] |>
    28.7 -  Pretty.setmp_margin (!margin)) p;
    28.8 +  Pretty.setmp_margin_CRITICAL (!margin)) p;
    28.9  
   28.10  val str = PrintMode.setmp [] Pretty.str;
   28.11  
   28.12 @@ -280,7 +280,7 @@
   28.13    let
   28.14      val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
   28.15      (* fake definition *)
   28.16 -    val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   28.17 +    val eq = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
   28.18        (Logic.mk_equals (x, t));
   28.19      fun err () = error "preprocess_term: bad preprocessor"
   28.20    in case map prop_of (preprocess thy [eq]) of
   28.21 @@ -883,7 +883,7 @@
   28.22  fun test_term ctxt t =
   28.23    let
   28.24      val thy = ProofContext.theory_of ctxt;
   28.25 -    val (code, gr) = setmp mode ["term_of", "test"]
   28.26 +    val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
   28.27        (generate_code_i thy [] "Generated") [("testf", t)];
   28.28      val Ts = map snd (fst (strip_abs t));
   28.29      val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
   28.30 @@ -923,7 +923,7 @@
   28.31            error "Term to be evaluated contains type variables";
   28.32          val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
   28.33            error "Term to be evaluated contains variables";
   28.34 -        val (code, gr) = setmp mode ["term_of"]
   28.35 +        val (code, gr) = setmp_CRITICAL mode ["term_of"]
   28.36            (generate_code_i thy [] "Generated")
   28.37            [("result", Abs ("x", TFree ("'a", []), t))];
   28.38          val s = "structure EvalTerm =\nstruct\n\n" ^
   28.39 @@ -1010,7 +1010,7 @@
   28.40    (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
   28.41      let
   28.42        val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
   28.43 -      val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs;
   28.44 +      val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
   28.45        val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
   28.46          (case opt_fname of
   28.47            NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
    29.1 --- a/src/Pure/goal_display.ML	Sat Oct 17 15:55:57 2009 +0200
    29.2 +++ b/src/Pure/goal_display.ML	Sat Oct 17 15:57:51 2009 +0200
    29.3 @@ -108,9 +108,9 @@
    29.4        (if types then pretty_vars prop else []) @
    29.5        (if sorts then pretty_varsT prop else []);
    29.6    in
    29.7 -    setmp show_no_free_types true
    29.8 -      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
    29.9 -        (setmp show_sorts false pretty_gs))
   29.10 +    setmp_CRITICAL show_no_free_types true
   29.11 +      (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   29.12 +        (setmp_CRITICAL show_sorts false pretty_gs))
   29.13     (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   29.14    end;
   29.15  
    30.1 --- a/src/Pure/library.ML	Sat Oct 17 15:55:57 2009 +0200
    30.2 +++ b/src/Pure/library.ML	Sat Oct 17 15:57:51 2009 +0200
    30.3 @@ -58,7 +58,7 @@
    30.4    val exists: ('a -> bool) -> 'a list -> bool
    30.5    val forall: ('a -> bool) -> 'a list -> bool
    30.6    val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    30.7 -  val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    30.8 +  val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
    30.9    val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
   30.10  
   30.11    (*lists*)
   30.12 @@ -329,7 +329,7 @@
   30.13        val _ = flag := orig_value;
   30.14      in Exn.release result end) ();
   30.15  
   30.16 -fun setmp flag value f x =
   30.17 +fun setmp_CRITICAL flag value f x =
   30.18    NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
   30.19  
   30.20  fun setmp_thread_data tag orig_data data f x =
    31.1 --- a/src/Pure/old_goals.ML	Sat Oct 17 15:55:57 2009 +0200
    31.2 +++ b/src/Pure/old_goals.ML	Sat Oct 17 15:57:51 2009 +0200
    31.3 @@ -367,9 +367,9 @@
    31.4  (*Two variants: one checking the result, one not.
    31.5    Neither prints runtime messages: they are for internal packages.*)
    31.6  fun prove_goalw_cterm rths chorn =
    31.7 -        setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
    31.8 +        setmp_CRITICAL Output.timing false (prove_goalw_cterm_general true rths chorn)
    31.9  and prove_goalw_cterm_nocheck rths chorn =
   31.10 -        setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
   31.11 +        setmp_CRITICAL Output.timing false (prove_goalw_cterm_general false rths chorn);
   31.12  
   31.13  
   31.14  (*Version taking the goal as a string*)
    32.1 --- a/src/Pure/theory.ML	Sat Oct 17 15:55:57 2009 +0200
    32.2 +++ b/src/Pure/theory.ML	Sat Oct 17 15:57:51 2009 +0200
    32.3 @@ -237,7 +237,7 @@
    32.4    in
    32.5      if Sign.typ_instance thy (declT, T') then ()
    32.6      else if Type.raw_instance (declT, T') then
    32.7 -      error (Library.setmp show_sorts true
    32.8 +      error (setmp_CRITICAL show_sorts true
    32.9          message "imposes additional sort constraints on the constant declaration")
   32.10      else if overloaded then ()
   32.11      else warning (message "is strictly less general than the declared type");
    33.1 --- a/src/Tools/Code/code_target.ML	Sat Oct 17 15:55:57 2009 +0200
    33.2 +++ b/src/Tools/Code/code_target.ML	Sat Oct 17 15:57:51 2009 +0200
    33.3 @@ -60,9 +60,9 @@
    33.4  type serialization = destination -> (string * string option list) option;
    33.5  
    33.6  val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
    33.7 -fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
    33.8 +fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL (!code_width) f);
    33.9  fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
   33.10 -fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
   33.11 +fun code_writeln p = Pretty.setmp_margin_CRITICAL (!code_width) Pretty.writeln p;
   33.12  
   33.13  (*FIXME why another code_setmp?*)
   33.14  fun compile f = (code_setmp f Compile; ());
    34.1 --- a/src/Tools/auto_solve.ML	Sat Oct 17 15:55:57 2009 +0200
    34.2 +++ b/src/Tools/auto_solve.ML	Sat Oct 17 15:57:51 2009 +0200
    34.3 @@ -27,7 +27,7 @@
    34.4  
    34.5  val _ =
    34.6    ProofGeneralPgip.add_preference Preferences.category_tracing
    34.7 -  (setmp auto true (fn () =>
    34.8 +  (setmp_CRITICAL auto true (fn () =>
    34.9      Preferences.bool_pref auto
   34.10        "auto-solve"
   34.11        "Try to solve newly declared lemmas with existing theorems.") ());
    35.1 --- a/src/Tools/nbe.ML	Sat Oct 17 15:55:57 2009 +0200
    35.2 +++ b/src/Tools/nbe.ML	Sat Oct 17 15:57:51 2009 +0200
    35.3 @@ -544,8 +544,8 @@
    35.4        (TypeInfer.constrain ty' t);
    35.5      fun check_tvars t = if null (Term.add_tvars t []) then t else
    35.6        error ("Illegal schematic type variables in normalized term: "
    35.7 -        ^ setmp show_types true (Syntax.string_of_term_global thy) t);
    35.8 -    val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
    35.9 +        ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
   35.10 +    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
   35.11    in
   35.12      compile_eval thy naming program (vs, t) deps
   35.13      |> traced (fn t => "Normalized:\n" ^ string_of_term t)
    36.1 --- a/src/Tools/quickcheck.ML	Sat Oct 17 15:55:57 2009 +0200
    36.2 +++ b/src/Tools/quickcheck.ML	Sat Oct 17 15:57:51 2009 +0200
    36.3 @@ -24,7 +24,7 @@
    36.4  
    36.5  val _ =
    36.6    ProofGeneralPgip.add_preference Preferences.category_tracing
    36.7 -  (setmp auto true (fn () =>
    36.8 +  (setmp_CRITICAL auto true (fn () =>
    36.9      Preferences.bool_pref auto
   36.10        "auto-quickcheck"
   36.11        "Whether to enable quickcheck automatically.") ());