# HG changeset patch
# User wenzelm
# Date 1220390864 -7200
# Node ID 7650d5e0f8fb89c2a58536abc5df68adad5b4feb
# Parent  fb16a07d6580f215dda0454f7ba7aa9ebd47fb88
refined theorem dependency output: previous state needs to contain a theory (not empty toplevel);
new_thms_deps: explicity theory values;

diff -r fb16a07d6580 -r 7650d5e0f8fb src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 02 22:41:36 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 02 23:27:44 2008 +0200
@@ -177,7 +177,9 @@
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
   if print_mode_active thm_depsN andalso Toplevel.is_theory state' andalso is_none opt_err then
-    let val (names, deps) = ProofGeneralPgip.new_thms_deps state state' in
+    let val (names, deps) =
+      ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
+    in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)
     end
diff -r fb16a07d6580 -r 7650d5e0f8fb src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 22:41:36 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 23:27:44 2008 +0200
@@ -8,7 +8,7 @@
 
 signature PROOF_GENERAL_PGIP =
 sig
-  val new_thms_deps: Toplevel.state -> Toplevel.state -> string list * string list
+  val new_thms_deps: theory -> theory -> string list * string list
   val init_pgip: bool -> unit             (* main PGIP loop with true; fail with false *)
 
   (* These two are just to support the semi-PGIP Emacs mode *)
@@ -267,12 +267,11 @@
 
 in
 
-fun new_thms_deps state state' =
+fun new_thms_deps thy thy' =
   let
-    val prev_facts =
-      (case try Toplevel.theory_of state of NONE => [] | SOME thy => [PureThy.facts_of thy]);
-    val facts = PureThy.facts_of (Toplevel.theory_of state');
-  in thms_deps (maps #2 (Facts.dest_static prev_facts facts)) end;
+    val prev_facts = PureThy.facts_of thy;
+    val facts = PureThy.facts_of thy';
+  in thms_deps (maps #2 (Facts.dest_static [prev_facts] facts)) end;
 
 end;
 
@@ -298,8 +297,11 @@
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
-  if ! show_theorem_dependencies andalso Toplevel.is_theory state' andalso is_none opt_err then
-    let val (names, deps) = new_thms_deps state state' in
+  if ! show_theorem_dependencies andalso
+    can Toplevel.theory_of state andalso
+    Toplevel.is_theory state' andalso is_none opt_err
+  then
+    let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
       if null names orelse null deps then ()
       else thm_deps_message (spaces_quote names, spaces_quote deps)
     end