change print_mode: CRITICAL;
authorwenzelm
Mon Sep 17 16:36:45 2007 +0200 (2007-09-17)
changeset 24614a4b2eb0dd673
parent 24613 bc889c3d55a3
child 24615 17dbd993293d
change print_mode: CRITICAL;
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/ProofGeneral/preferences.ML	Mon Sep 17 16:36:43 2007 +0200
     1.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Mon Sep 17 16:36:45 2007 +0200
     1.3 @@ -67,10 +67,11 @@
     1.4  val thm_deps_pref =
     1.5      let
     1.6          fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
     1.7 -        fun set s = if PgipTypes.read_pgipbool s then
     1.8 -                        change print_mode (insert (op =) thm_depsN)
     1.9 -                    else
    1.10 -                        change print_mode (remove (op =) thm_depsN)
    1.11 +        fun set s =  NAMED_CRITICAL "print_mode" (fn () =>
    1.12 +          if PgipTypes.read_pgipbool s then
    1.13 +            change print_mode (insert (op =) thm_depsN)
    1.14 +          else
    1.15 +            change print_mode (remove (op =) thm_depsN))
    1.16      in
    1.17          mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
    1.18                 "Track theorem dependencies within Proof General"
     2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 17 16:36:43 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Sep 17 16:36:45 2007 +0200
     2.3 @@ -572,9 +572,10 @@
     2.4  
     2.5  fun set_proverflag_pgmlsymbols b =
     2.6      (pgmlsymbols_flag := b;
     2.7 -     change print_mode 
     2.8 +      NAMED_CRITICAL "print_mode" (fn () =>
     2.9 +        change print_mode 
    2.10              (fn mode =>
    2.11 -                remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else [])))
    2.12 +                remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))))
    2.13  
    2.14  fun set_proverflag_thmdeps b =
    2.15      (show_theorem_dependencies := b;