# 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;