# HG changeset patch # User wenzelm # Date 1255787871 -7200 # Node ID 5b21661fe618353ba340a09dc580528816606410 # Parent ecb746bca732f1ce4ffdaf2d7a032c1df853f144 indicate CRITICAL nature of various setmp combinators; diff -r ecb746bca732 -r 5b21661fe618 doc-src/IsarImplementation/Thy/ML.thy --- 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 diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Import/proof_kernel.ML --- 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 "^ diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Import/replay.ML --- 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 diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Statespace/state_space.ML --- 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 => [] diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Function/fundef_common.ML --- 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 diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- 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 diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML --- 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 diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- 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' diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 = diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/res_reconstruct.ML --- 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'); diff -r ecb746bca732 -r 5b21661fe618 src/HOL/Tools/typedef.ML --- 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 => diff -r ecb746bca732 -r 5b21661fe618 src/Pure/General/output.ML --- 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 () diff -r ecb746bca732 -r 5b21661fe618 src/Pure/General/pretty.ML --- 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 *) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/class_target.ML --- 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: ", diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/code.ML --- 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) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/method.ML --- 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)))); diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/obtain.ML --- 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); diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/proof_context.ML --- 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 *) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Isar/skip_proof.ML --- 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 = diff -r ecb746bca732 -r 5b21661fe618 src/Pure/ML/ml_context.ML --- 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; diff -r ecb746bca732 -r 5b21661fe618 src/Pure/ProofGeneral/preferences.ML --- 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") (), diff -r ecb746bca732 -r 5b21661fe618 src/Pure/ProofGeneral/proof_general_emacs.ML --- 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; diff -r ecb746bca732 -r 5b21661fe618 src/Pure/ProofGeneral/proof_general_pgip.ML --- 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 (" 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 diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Syntax/printer.ML --- 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); diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Thy/thy_load.ML --- 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 = diff -r ecb746bca732 -r 5b21661fe618 src/Pure/Thy/thy_output.ML --- 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 *) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/axclass.ML --- 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); diff -r ecb746bca732 -r 5b21661fe618 src/Pure/codegen.ML --- 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)) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/goal_display.ML --- 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; diff -r ecb746bca732 -r 5b21661fe618 src/Pure/library.ML --- 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 = diff -r ecb746bca732 -r 5b21661fe618 src/Pure/old_goals.ML --- 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*) diff -r ecb746bca732 -r 5b21661fe618 src/Pure/theory.ML --- 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"); diff -r ecb746bca732 -r 5b21661fe618 src/Tools/Code/code_target.ML --- 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; ()); diff -r ecb746bca732 -r 5b21661fe618 src/Tools/auto_solve.ML --- 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.") ()); diff -r ecb746bca732 -r 5b21661fe618 src/Tools/nbe.ML --- 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) diff -r ecb746bca732 -r 5b21661fe618 src/Tools/quickcheck.ML --- 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.") ());