# HG changeset patch # User wenzelm # Date 1190039805 -7200 # Node ID a4b2eb0dd6737ef6c34f10a10d70f04a51c27359 # Parent bc889c3d55a3d19344aaa446f5a2b1750f7827f5 change print_mode: CRITICAL; diff -r bc889c3d55a3 -r a4b2eb0dd673 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Mon Sep 17 16:36:43 2007 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Mon Sep 17 16:36:45 2007 +0200 @@ -67,10 +67,11 @@ val thm_deps_pref = let fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN) - fun set s = if PgipTypes.read_pgipbool s then - change print_mode (insert (op =) thm_depsN) - else - change print_mode (remove (op =) thm_depsN) + fun set s = NAMED_CRITICAL "print_mode" (fn () => + if PgipTypes.read_pgipbool s then + change print_mode (insert (op =) thm_depsN) + else + change print_mode (remove (op =) thm_depsN)) in mkpref get set PgipTypes.Pgipbool "theorem-dependencies" "Track theorem dependencies within Proof General" diff -r bc889c3d55a3 -r a4b2eb0dd673 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 17 16:36:43 2007 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Sep 17 16:36:45 2007 +0200 @@ -572,9 +572,10 @@ fun set_proverflag_pgmlsymbols b = (pgmlsymbols_flag := b; - change print_mode + NAMED_CRITICAL "print_mode" (fn () => + change print_mode (fn mode => - remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))) + remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))) fun set_proverflag_thmdeps b = (show_theorem_dependencies := b;