--- a/doc-src/IsarImplementation/Thy/ML.thy Sat Oct 17 15:55:57 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Sat Oct 17 15:57:51 2009 +0200
@@ -229,7 +229,7 @@
view being presented to the user.
Occasionally, such global process flags are treated like implicit
- arguments to certain operations, by using the @{ML setmp} combinator
+ arguments to certain operations, by using the @{ML setmp_CRITICAL} combinator
for safe temporary assignment. Its traditional purpose was to
ensure proper recovery of the original value when exceptions are
raised in the body, now the functionality is extended to enter the
@@ -237,7 +237,7 @@
parallelism).
Note that recovery of plain value passing semantics via @{ML
- setmp}~@{text "ref value"} assumes that this @{text "ref"} is
+ setmp_CRITICAL}~@{text "ref value"} assumes that this @{text "ref"} is
exclusively manipulated within the critical section. In particular,
any persistent global assignment of @{text "ref := value"} needs to
be marked critical as well, to prevent intruding another threads
@@ -258,7 +258,7 @@
\begin{mldecls}
@{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
@{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
- @{index_ML setmp: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
+ @{index_ML setmp_CRITICAL: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
\end{mldecls}
\begin{description}
@@ -272,7 +272,7 @@
\item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
name argument.
- \item @{ML setmp}~@{text "ref value f x"} evaluates @{text "f x"}
+ \item @{ML setmp_CRITICAL}~@{text "ref value f x"} evaluates @{text "f x"}
while staying within the critical section and having @{text "ref :=
value"} assigned temporarily. This recovers a value-passing
semantics involving global references, regardless of exceptions or
--- a/src/HOL/Import/proof_kernel.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sat Oct 17 15:57:51 2009 +0200
@@ -201,10 +201,10 @@
in
quote (
PrintMode.setmp [] (
- Library.setmp show_brackets false (
- Library.setmp show_all_types true (
- Library.setmp Syntax.ambiguity_is_error false (
- Library.setmp show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
+ setmp_CRITICAL show_brackets false (
+ setmp_CRITICAL show_all_types true (
+ setmp_CRITICAL Syntax.ambiguity_is_error false (
+ setmp_CRITICAL show_sorts true (Syntax.string_of_term_global thy o Thm.term_of)))))
ct)
end
@@ -219,15 +219,15 @@
val ct = (cterm_of thy (HOLogic.dest_Trueprop t)
handle TERM _ => ct)
fun match u = t aconv u
- fun G 0 = Library.setmp show_types true (Library.setmp show_sorts true)
- | G 1 = Library.setmp show_brackets true (G 0)
- | G 2 = Library.setmp show_all_types true (G 0)
- | G 3 = Library.setmp show_brackets true (G 2)
+ fun G 0 = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true)
+ | G 1 = setmp_CRITICAL show_brackets true (G 0)
+ | G 2 = setmp_CRITICAL show_all_types true (G 0)
+ | G 3 = setmp_CRITICAL show_brackets true (G 2)
| G _ = raise SMART_STRING
fun F n =
let
val str =
- Library.setmp show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
+ setmp_CRITICAL show_brackets false (G n (Syntax.string_of_term ctxt o term_of)) ct
val u = Syntax.parse_term ctxt str
|> TypeInfer.constrain T |> Syntax.check_term ctxt
in
@@ -239,7 +239,7 @@
| SMART_STRING =>
error ("smart_string failed for: "^ G 0 (Syntax.string_of_term ctxt o term_of) ct)
in
- PrintMode.setmp [] (Library.setmp Syntax.ambiguity_is_error true F) 0
+ PrintMode.setmp [] (setmp_CRITICAL Syntax.ambiguity_is_error true F) 0
end
handle ERROR mesg => simple_smart_string_of_cterm ct
@@ -2124,7 +2124,7 @@
else "(" ^ commas tnames ^ ") "
val proc_prop = if null tnames
then smart_string_of_cterm
- else Library.setmp show_all_types true smart_string_of_cterm
+ else setmp_CRITICAL show_all_types true smart_string_of_cterm
val thy5 = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^ " = " ^ (proc_prop (cterm_of thy4 c)) ^ " "
^ (string_of_mixfix tsyn) ^ "\n by (rule typedef_helper,import " ^ thyname ^ " " ^ thmname ^ ")") thy4
@@ -2219,7 +2219,7 @@
else "(" ^ commas tnames ^ ") "
val proc_prop = if null tnames
then smart_string_of_cterm
- else Library.setmp show_all_types true smart_string_of_cterm
+ else setmp_CRITICAL show_all_types true smart_string_of_cterm
val thy = add_dump ("typedef (open) " ^ tnames_string ^ (quotename tycname) ^
" = " ^ (proc_prop (cterm_of thy4 c)) ^ " " ^
(string_of_mixfix tsyn) ^ " morphisms "^
--- a/src/HOL/Import/replay.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Import/replay.ML Sat Oct 17 15:57:51 2009 +0200
@@ -320,7 +320,7 @@
fun replay_chached_thm int_thms thyname thmname =
let
- fun th_of thy = setmp quick_and_dirty true (SkipProof.make_thm thy)
+ fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
fun err msg = raise ERR "replay_cached_thm" msg
val _ = writeln ("Replaying (from cache) "^thmname^" ...")
fun rps [] thy = thy
--- a/src/HOL/Statespace/state_space.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML Sat Oct 17 15:57:51 2009 +0200
@@ -297,7 +297,7 @@
val tt' = tt |> fold upd all_names;
val activate_simproc =
- Output.no_warnings
+ Output.no_warnings_CRITICAL
(Simplifier.map_ss (fn ss => ss addsimprocs [distinct_simproc]));
val ctxt' =
ctxt
@@ -444,7 +444,7 @@
in Context.mapping I upd_prf ctxt end;
fun string_of_typ T =
- setmp show_sorts true
+ setmp_CRITICAL show_sorts true
(PrintMode.setmp [] (Syntax.string_of_typ (ProofContext.init thy))) T;
val fixestate = (case state_type of
NONE => []
--- a/src/HOL/Tools/Function/fundef_common.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_common.ML Sat Oct 17 15:57:51 2009 +0200
@@ -267,7 +267,7 @@
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
orelse error (cat_lines
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
- setmp show_sorts true (Syntax.string_of_typ ctxt) fT])
+ setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
val _ = map check_sorts fixes
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 17 15:57:51 2009 +0200
@@ -108,7 +108,7 @@
in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt
val t' = Pattern.rewrite_term thy rewr [] t
- val tac = setmp quick_and_dirty true (SkipProof.cheat_tac thy)
+ val tac = setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy)
val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML Sat Oct 17 15:57:51 2009 +0200
@@ -56,7 +56,7 @@
val ((_, intros), ctxt') = Variable.import true intros ctxt
val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
(flatten constname) (map prop_of intros) ([], thy)
- val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
+ val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
|> Variable.export ctxt' ctxt
in
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 17 15:57:51 2009 +0200
@@ -58,7 +58,7 @@
val t = Logic.list_implies
(map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
- val tac = fn {...} => setmp quick_and_dirty true (SkipProof.cheat_tac thy')
+ val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
val _ = tracing (Display.string_of_thm ctxt' intro)
val thy'' = thy'
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 17 15:57:51 2009 +0200
@@ -661,7 +661,7 @@
val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
val nparams = guess_nparams T
val pre_elim =
- (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy)))
+ (Drule.standard o (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)))
(mk_casesrule (ProofContext.init thy) nparams pre_intros)
in register_predicate (pre_intros, pre_elim, nparams) thy end
@@ -2077,12 +2077,12 @@
(if !do_proofs then
(fn _ =>
rtac @{thm pred_iffI} 1
- THEN print_tac "after pred_iffI"
+ THEN print_tac "after pred_iffI"
THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
THEN print_tac "proved one direction"
THEN prove_other_direction thy modes pred mode moded_clauses
THEN print_tac "proved other direction")
- else (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy))
+ else (fn _ => setmp_CRITICAL quick_and_dirty true SkipProof.cheat_tac thy))
end;
(* composition of mode inference, definition, compilation and proof *)
@@ -2110,7 +2110,8 @@
(join_preds_modes moded_clauses compiled_terms)
fun prove_by_skip thy _ _ _ _ compiled_terms =
- map_preds_modes (fn pred => fn mode => fn t => Drule.standard (setmp quick_and_dirty true (SkipProof.make_thm thy) t))
+ map_preds_modes (fn pred => fn mode => fn t =>
+ Drule.standard (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy) t))
compiled_terms
fun prepare_intrs thy prednames =
--- a/src/HOL/Tools/res_reconstruct.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sat Oct 17 15:57:51 2009 +0200
@@ -354,7 +354,7 @@
"\"\n by (metis " ^ space_implode " " deps ^ ")\n"
fun dolines [(lname, t, deps)] = [doline "show " (lname, t, deps)]
| dolines ((lname, t, deps)::lines) = doline "have " (lname, t, deps) :: dolines lines
- in setmp show_sorts (Config.get ctxt recon_sorts) dolines end;
+ in setmp_CRITICAL show_sorts (Config.get ctxt recon_sorts) dolines end;
fun notequal t (_,t',_) = not (t aconv t');
--- a/src/HOL/Tools/typedef.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/HOL/Tools/typedef.ML Sat Oct 17 15:57:51 2009 +0200
@@ -200,7 +200,7 @@
(*test theory errors now!*)
val test_thy = Theory.copy thy;
val _ = test_thy
- |> typedef_result (setmp quick_and_dirty true (SkipProof.make_thm test_thy) goal);
+ |> typedef_result (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm test_thy) goal);
in (set, goal, goal_pat, typedef_result) end
handle ERROR msg =>
--- a/src/Pure/General/output.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/General/output.ML Sat Oct 17 15:57:51 2009 +0200
@@ -44,7 +44,7 @@
val prompt: string -> unit
val status: string -> unit
val debugging: bool Unsynchronized.ref
- val no_warnings: ('a -> 'b) -> 'a -> 'b
+ val no_warnings_CRITICAL: ('a -> 'b) -> 'a -> 'b
val debug: (unit -> string) -> unit
end;
@@ -112,7 +112,7 @@
fun legacy_feature s =
(if ! tolerate_legacy_features then warning else error) ("Legacy feature! " ^ s);
-fun no_warnings f = setmp warning_fn (K ()) f;
+fun no_warnings_CRITICAL f = setmp_CRITICAL warning_fn (K ()) f;
val debugging = Unsynchronized.ref false;
fun debug s = if ! debugging then ! debug_fn (output (s ())) else ()
--- a/src/Pure/General/pretty.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/General/pretty.ML Sat Oct 17 15:57:51 2009 +0200
@@ -53,7 +53,7 @@
val indent: int -> T -> T
val unbreakable: T -> T
val setmargin: int -> unit
- val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
+ val setmp_margin_CRITICAL: int -> ('a -> 'b) -> 'a -> 'b
val setdepth: int -> unit
val to_ML: T -> ML_Pretty.pretty
val from_ML: ML_Pretty.pretty -> T
@@ -188,7 +188,7 @@
val margin_info = Unsynchronized.ref (make_margin_info 76);
fun setmargin m = margin_info := make_margin_info m;
-fun setmp_margin m f = setmp margin_info (make_margin_info m) f;
+fun setmp_margin_CRITICAL m f = setmp_CRITICAL margin_info (make_margin_info m) f;
(* depth limitation *)
--- a/src/Pure/Isar/class_target.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/class_target.ML Sat Oct 17 15:57:51 2009 +0200
@@ -177,7 +177,7 @@
val Ss = Sorts.mg_domain algebra tyco [class];
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
- ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
+ ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
--- a/src/Pure/Isar/code.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/code.ML Sat Oct 17 15:57:51 2009 +0200
@@ -94,7 +94,7 @@
(* printing *)
-fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy);
+fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
--- a/src/Pure/Isar/method.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/method.ML Sat Oct 17 15:57:51 2009 +0200
@@ -151,7 +151,7 @@
(* cheating *)
-fun cheating int ctxt = METHOD (K (setmp quick_and_dirty (int orelse ! quick_and_dirty)
+fun cheating int ctxt = METHOD (K (setmp_CRITICAL quick_and_dirty (int orelse ! quick_and_dirty)
(SkipProof.cheat_tac (ProofContext.theory_of ctxt))));
--- a/src/Pure/Isar/obtain.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Oct 17 15:57:51 2009 +0200
@@ -215,7 +215,7 @@
val thy = ProofContext.theory_of ctxt;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
- val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
+ val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
--- a/src/Pure/Isar/proof_context.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/proof_context.ML Sat Oct 17 15:57:51 2009 +0200
@@ -366,7 +366,7 @@
(case try Name.dest_skolem x of
NONE => Pretty.mark Markup.var (Pretty.str s)
| SOME x' => Pretty.mark Markup.skolem
- (Pretty.str (setmp show_question_marks true Term.string_of_vname (x', i))))
+ (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
| NONE => Pretty.mark Markup.var (Pretty.str s));
fun class_markup _ c = (* FIXME authentic name *)
@@ -1213,7 +1213,7 @@
val verbose = Unsynchronized.ref false;
fun verb f x = if ! verbose then f (x ()) else [];
-fun setmp_verbose f x = Library.setmp verbose true f x;
+fun setmp_verbose f x = setmp_CRITICAL verbose true f x;
(* local syntax *)
--- a/src/Pure/Isar/skip_proof.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Isar/skip_proof.ML Sat Oct 17 15:57:51 2009 +0200
@@ -36,7 +36,7 @@
(if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
(fn args => fn st =>
if ! quick_and_dirty
- then setmp quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
+ then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
else tac args st);
fun prove_global thy xs asms prop tac =
--- a/src/Pure/ML/ml_context.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/ML/ml_context.ML Sat Oct 17 15:57:51 2009 +0200
@@ -64,7 +64,7 @@
if name = "" then ()
else if not (ML_Syntax.is_identifier name) then
error ("Cannot bind theorem(s) " ^ quote name ^ " as ML value")
- else setmp stored_thms ths' (fn () =>
+ else setmp_CRITICAL stored_thms ths' (fn () =>
ML_Compiler.eval true Position.none
(ML_Lex.tokenize ("val " ^ name ^ " = " ^ sel ^ "(! ML_Context.stored_thms);"))) ();
in () end;
--- a/src/Pure/ProofGeneral/preferences.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Sat Oct 17 15:57:51 2009 +0200
@@ -78,7 +78,7 @@
(* preferences of Pure *)
-val proof_pref = setmp Proofterm.proofs 1 (fn () =>
+val proof_pref = setmp_CRITICAL Proofterm.proofs 1 (fn () =>
let
fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
@@ -167,7 +167,7 @@
thm_deps_pref];
val proof_preferences =
- [setmp quick_and_dirty true (fn () =>
+ [setmp_CRITICAL quick_and_dirty true (fn () =>
bool_pref quick_and_dirty
"quick-and-dirty"
"Take a few short cuts") (),
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Sat Oct 17 15:57:51 2009 +0200
@@ -231,7 +231,7 @@
fun init false = panic "No Proof General interface support for Isabelle/classic mode."
| init true =
(! initialized orelse
- (Output.no_warnings init_outer_syntax ();
+ (Output.no_warnings_CRITICAL init_outer_syntax ();
Output.add_mode Symbol.xsymbolsN Symbol.output Output.default_escape;
Output.add_mode proof_generalN Output.default_output Output.default_escape;
Markup.add_mode proof_generalN YXML.output_markup;
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Oct 17 15:57:51 2009 +0200
@@ -807,7 +807,8 @@
val filepath = PgipTypes.path_of_pgipurl url
val filedir = Path.dir filepath
val thy_name = Path.implode o #1 o Path.split_ext o Path.base
- val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
+ val openfile_retract = Output.no_warnings_CRITICAL
+ (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
in
case !currently_open_file of
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
@@ -1030,7 +1031,7 @@
Output.add_mode proof_generalN Output.default_output Output.default_escape;
Markup.add_mode proof_generalN YXML.output_markup;
setup_messages ();
- Output.no_warnings init_outer_syntax ();
+ Output.no_warnings_CRITICAL init_outer_syntax ();
setup_thy_loader ();
setup_present_hook ();
init_pgip_session_id ();
@@ -1057,7 +1058,7 @@
This works for preferences but not generally guaranteed
because we haven't done full setup here (e.g., no pgml mode) *)
fun process_pgip str =
- setmp output_xml_fn (!pgip_output_channel) process_pgip_plain str
+ setmp_CRITICAL output_xml_fn (!pgip_output_channel) process_pgip_plain str
end
--- a/src/Pure/Syntax/printer.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Syntax/printer.ML Sat Oct 17 15:57:51 2009 +0200
@@ -48,7 +48,7 @@
val show_no_free_types = Unsynchronized.ref false;
val show_all_types = Unsynchronized.ref false;
-fun pp_show_brackets pp = Pretty.pp (setmp show_brackets true (Pretty.term pp),
+fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
--- a/src/Pure/Thy/thy_load.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML Sat Oct 17 15:57:51 2009 +0200
@@ -50,7 +50,7 @@
fun reset_path () = load_path := [Path.current];
fun with_paths ss f x =
- CRITICAL (fn () => Library.setmp load_path (! load_path @ map Path.explode ss) f x);
+ CRITICAL (fn () => setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
fun with_path s f x = with_paths [s] f x;
fun search_path dir path =
--- a/src/Pure/Thy/thy_output.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/Thy/thy_output.ML Sat Oct 17 15:57:51 2009 +0200
@@ -154,7 +154,7 @@
let val (opts, src) = T.read_antiq lex antiq (ss, pos) in
options opts (fn () => command src state) (); (*preview errors!*)
PrintMode.with_modes (! modes @ Latex.modes)
- (Output.no_warnings (options opts (fn () => command src state))) ()
+ (Output.no_warnings_CRITICAL (options opts (fn () => command src state))) ()
end
| expand (Antiquote.Open _) = ""
| expand (Antiquote.Close _) = "";
@@ -416,22 +416,22 @@
(* options *)
val _ = add_options
- [("show_types", Library.setmp Syntax.show_types o boolean),
- ("show_sorts", Library.setmp Syntax.show_sorts o boolean),
- ("show_structs", Library.setmp show_structs o boolean),
- ("show_question_marks", Library.setmp show_question_marks o boolean),
- ("long_names", Library.setmp NameSpace.long_names o boolean),
- ("short_names", Library.setmp NameSpace.short_names o boolean),
- ("unique_names", Library.setmp NameSpace.unique_names o boolean),
- ("eta_contract", Library.setmp Syntax.eta_contract o boolean),
- ("display", Library.setmp display o boolean),
- ("break", Library.setmp break o boolean),
- ("quotes", Library.setmp quotes o boolean),
+ [("show_types", setmp_CRITICAL Syntax.show_types o boolean),
+ ("show_sorts", setmp_CRITICAL Syntax.show_sorts o boolean),
+ ("show_structs", setmp_CRITICAL show_structs o boolean),
+ ("show_question_marks", setmp_CRITICAL show_question_marks o boolean),
+ ("long_names", setmp_CRITICAL NameSpace.long_names o boolean),
+ ("short_names", setmp_CRITICAL NameSpace.short_names o boolean),
+ ("unique_names", setmp_CRITICAL NameSpace.unique_names o boolean),
+ ("eta_contract", setmp_CRITICAL Syntax.eta_contract o boolean),
+ ("display", setmp_CRITICAL display o boolean),
+ ("break", setmp_CRITICAL break o boolean),
+ ("quotes", setmp_CRITICAL quotes o boolean),
("mode", fn s => fn f => PrintMode.with_modes [s] f),
- ("margin", Pretty.setmp_margin o integer),
- ("indent", Library.setmp indent o integer),
- ("source", Library.setmp source o boolean),
- ("goals_limit", Library.setmp goals_limit o integer)];
+ ("margin", Pretty.setmp_margin_CRITICAL o integer),
+ ("indent", setmp_CRITICAL indent o integer),
+ ("source", setmp_CRITICAL source o boolean),
+ ("goals_limit", setmp_CRITICAL goals_limit o integer)];
(* basic pretty printing *)
--- a/src/Pure/axclass.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/axclass.ML Sat Oct 17 15:57:51 2009 +0200
@@ -438,7 +438,7 @@
fun check_constraint (a, S) =
if Sign.subsort thy (super, S) then ()
else error ("Sort constraint of type variable " ^
- setmp show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
+ setmp_CRITICAL show_sorts true (Pretty.string_of_typ pp) (TFree (a, S)) ^
" needs to be weaker than " ^ Pretty.string_of_sort pp super);
--- a/src/Pure/codegen.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/codegen.ML Sat Oct 17 15:57:51 2009 +0200
@@ -111,7 +111,7 @@
fun string_of p = (Pretty.string_of |>
PrintMode.setmp [] |>
- Pretty.setmp_margin (!margin)) p;
+ Pretty.setmp_margin_CRITICAL (!margin)) p;
val str = PrintMode.setmp [] Pretty.str;
@@ -280,7 +280,7 @@
let
val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
(* fake definition *)
- val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
+ val eq = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
(Logic.mk_equals (x, t));
fun err () = error "preprocess_term: bad preprocessor"
in case map prop_of (preprocess thy [eq]) of
@@ -883,7 +883,7 @@
fun test_term ctxt t =
let
val thy = ProofContext.theory_of ctxt;
- val (code, gr) = setmp mode ["term_of", "test"]
+ val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
(generate_code_i thy [] "Generated") [("testf", t)];
val Ts = map snd (fst (strip_abs t));
val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
@@ -923,7 +923,7 @@
error "Term to be evaluated contains type variables";
val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
error "Term to be evaluated contains variables";
- val (code, gr) = setmp mode ["term_of"]
+ val (code, gr) = setmp_CRITICAL mode ["term_of"]
(generate_code_i thy [] "Generated")
[("result", Abs ("x", TFree ("'a", []), t))];
val s = "structure EvalTerm =\nstruct\n\n" ^
@@ -1010,7 +1010,7 @@
(fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
let
val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
- val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs;
+ val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
(case opt_fname of
NONE => ML_Context.eval false Position.none (cat_lines (map snd code))
--- a/src/Pure/goal_display.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/goal_display.ML Sat Oct 17 15:57:51 2009 +0200
@@ -108,9 +108,9 @@
(if types then pretty_vars prop else []) @
(if sorts then pretty_varsT prop else []);
in
- setmp show_no_free_types true
- (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
- (setmp show_sorts false pretty_gs))
+ setmp_CRITICAL show_no_free_types true
+ (setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
+ (setmp_CRITICAL show_sorts false pretty_gs))
(! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
end;
--- a/src/Pure/library.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/library.ML Sat Oct 17 15:57:51 2009 +0200
@@ -58,7 +58,7 @@
val exists: ('a -> bool) -> 'a list -> bool
val forall: ('a -> bool) -> 'a list -> bool
val setmp_noncritical: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
- val setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
+ val setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c
val setmp_thread_data: 'a Universal.tag -> 'a -> 'a -> ('b -> 'c) -> 'b -> 'c
(*lists*)
@@ -329,7 +329,7 @@
val _ = flag := orig_value;
in Exn.release result end) ();
-fun setmp flag value f x =
+fun setmp_CRITICAL flag value f x =
NAMED_CRITICAL "setmp" (fn () => setmp_noncritical flag value f x);
fun setmp_thread_data tag orig_data data f x =
--- a/src/Pure/old_goals.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/old_goals.ML Sat Oct 17 15:57:51 2009 +0200
@@ -367,9 +367,9 @@
(*Two variants: one checking the result, one not.
Neither prints runtime messages: they are for internal packages.*)
fun prove_goalw_cterm rths chorn =
- setmp Output.timing false (prove_goalw_cterm_general true rths chorn)
+ setmp_CRITICAL Output.timing false (prove_goalw_cterm_general true rths chorn)
and prove_goalw_cterm_nocheck rths chorn =
- setmp Output.timing false (prove_goalw_cterm_general false rths chorn);
+ setmp_CRITICAL Output.timing false (prove_goalw_cterm_general false rths chorn);
(*Version taking the goal as a string*)
--- a/src/Pure/theory.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Pure/theory.ML Sat Oct 17 15:57:51 2009 +0200
@@ -237,7 +237,7 @@
in
if Sign.typ_instance thy (declT, T') then ()
else if Type.raw_instance (declT, T') then
- error (Library.setmp show_sorts true
+ error (setmp_CRITICAL show_sorts true
message "imposes additional sort constraints on the constant declaration")
else if overloaded then ()
else warning (message "is strictly less general than the declared type");
--- a/src/Tools/Code/code_target.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Tools/Code/code_target.ML Sat Oct 17 15:57:51 2009 +0200
@@ -60,9 +60,9 @@
type serialization = destination -> (string * string option list) option;
val code_width = Unsynchronized.ref 80; (*FIXME after Pretty module no longer depends on print mode*)
-fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin (!code_width) f);
+fun code_setmp f = PrintMode.setmp [] (Pretty.setmp_margin_CRITICAL (!code_width) f);
fun code_of_pretty p = code_setmp Pretty.string_of p ^ "\n";
-fun code_writeln p = Pretty.setmp_margin (!code_width) Pretty.writeln p;
+fun code_writeln p = Pretty.setmp_margin_CRITICAL (!code_width) Pretty.writeln p;
(*FIXME why another code_setmp?*)
fun compile f = (code_setmp f Compile; ());
--- a/src/Tools/auto_solve.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Tools/auto_solve.ML Sat Oct 17 15:57:51 2009 +0200
@@ -27,7 +27,7 @@
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (setmp auto true (fn () =>
+ (setmp_CRITICAL auto true (fn () =>
Preferences.bool_pref auto
"auto-solve"
"Try to solve newly declared lemmas with existing theorems.") ());
--- a/src/Tools/nbe.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Tools/nbe.ML Sat Oct 17 15:57:51 2009 +0200
@@ -544,8 +544,8 @@
(TypeInfer.constrain ty' t);
fun check_tvars t = if null (Term.add_tvars t []) then t else
error ("Illegal schematic type variables in normalized term: "
- ^ setmp show_types true (Syntax.string_of_term_global thy) t);
- val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
+ ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
+ val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
in
compile_eval thy naming program (vs, t) deps
|> traced (fn t => "Normalized:\n" ^ string_of_term t)
--- a/src/Tools/quickcheck.ML Sat Oct 17 15:55:57 2009 +0200
+++ b/src/Tools/quickcheck.ML Sat Oct 17 15:57:51 2009 +0200
@@ -24,7 +24,7 @@
val _ =
ProofGeneralPgip.add_preference Preferences.category_tracing
- (setmp auto true (fn () =>
+ (setmp_CRITICAL auto true (fn () =>
Preferences.bool_pref auto
"auto-quickcheck"
"Whether to enable quickcheck automatically.") ());