# HG changeset patch
# User wenzelm
# Date 1368643527 -7200
# Node ID 56dfc90a5c75f4cbfe3962506960c6f781df6ce6
# Parent  e91359bfc84abcf9dbb36b427b3668e3a7e28bcd
more elementary ProofGeneral.thm_deps;

diff -r e91359bfc84a -r 56dfc90a5c75 src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Wed May 15 20:39:25 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Wed May 15 20:45:27 2013 +0200
@@ -27,7 +27,7 @@
   val preference_option: category -> string -> string -> string -> unit
   structure ThyLoad: sig val add_path: string -> unit end
   val init: unit -> unit
-  val thm_depsN: string
+  val thm_deps: bool Unsynchronized.ref
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
@@ -357,7 +357,7 @@
 
 in
 
-fun thm_deps ths =
+fun get_thm_deps ths =
   let
     (* FIXME proper derivation names!? *)
     val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
@@ -369,7 +369,7 @@
 
 (* report via hook *)
 
-val thm_depsN = "thm_deps";
+val thm_deps = Unsynchronized.ref false;
 
 local
 
@@ -381,13 +381,12 @@
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
-  if print_mode_active thm_depsN andalso
-    can Toplevel.theory_of state andalso Toplevel.is_theory state'
+  if ! thm_deps andalso can Toplevel.theory_of state andalso Toplevel.is_theory state'
   then
     let
       val prev_facts = Global_Theory.facts_of (Toplevel.theory_of state);
       val facts = Global_Theory.facts_of (Toplevel.theory_of state');
-      val (names, deps) = thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
+      val (names, deps) = get_thm_deps (maps #2 (Facts.dest_static [prev_facts] facts));
     in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)
diff -r e91359bfc84a -r 56dfc90a5c75 src/Pure/Tools/proof_general_pure.ML
--- a/src/Pure/Tools/proof_general_pure.ML	Wed May 15 20:39:25 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed May 15 20:45:27 2013 +0200
@@ -106,13 +106,8 @@
     "Whether to enable debugging";
 
 val _ =
-  ProofGeneral.preference_raw ProofGeneral.category_tracing
-    (fn () => Markup.print_bool (print_mode_active ProofGeneral.thm_depsN))
-    (fn s =>
-      if Markup.parse_bool s
-      then Unsynchronized.change print_mode (insert (op =) ProofGeneral.thm_depsN)
-      else Unsynchronized.change print_mode (remove (op =) ProofGeneral.thm_depsN))
-    ProofGeneral.pgipbool
+  ProofGeneral.preference_bool ProofGeneral.category_tracing
+    ProofGeneral.thm_deps
     "theorem-dependencies"
     "Track theorem dependencies within Proof General";