# HG changeset patch
# User wenzelm
# Date 1220386827 -7200
# Node ID 003dff7410c14e5acee27750aba75c8d9ac67efc
# Parent  046418f6447456fb85d2c93eb7c19ea1ab81780d
added new_thms_deps (operates on global facts, some name_hint approximation);
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;

diff -r 046418f64474 -r 003dff7410c1 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 22:20:25 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Sep 02 22:20:27 2008 +0200
@@ -8,6 +8,7 @@
 
 signature PROOF_GENERAL_PGIP =
 sig
+  val new_thms_deps: Toplevel.state -> Toplevel.state -> 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 *)
@@ -245,7 +246,38 @@
      welcome ());
 
 
-(* theorem dependency output *)
+(* theorem dependencies *)
+
+local
+
+fun thm_deps th =
+  (case Thm.proof_of th of
+    PThm (name, prf, _, _) =>
+      if Thm.has_name_hint th andalso Thm.get_name_hint th = name then
+        Proofterm.thms_of_proof' prf
+      else I
+  | prf => Proofterm.thms_of_proof' prf);
+
+fun thms_deps ths =
+  let
+    (* FIXME proper derivation names!? *)
+    val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
+    val deps = Symtab.keys (fold thm_deps ths Symtab.empty);
+  in (names, deps) end;
+
+in
+
+fun new_thms_deps state state' =
+  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;
+
+end;
+
+
+(* theorem dependeny output *)
 
 val show_theorem_dependencies = ref false;
 
@@ -254,33 +286,28 @@
 val spaces_quote = space_implode " " o map quote;
 
 fun thm_deps_message (thms, deps) =
-    let
-        val valuethms = XML.Elem("value",[("name", "thms")],[XML.Text thms])
-        val valuedeps = XML.Elem("value",[("name", "deps")],[XML.Text deps])
-    in
-        issue_pgip (Metainforesponse {attrs=[("infotype", "isabelle_theorem_dependencies")],
-                                      content=[valuethms,valuedeps]})
-    end
-
-fun tell_thm_deps ths =
-  if !show_theorem_dependencies then
-      let
-        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
-        val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
-                                        (map Thm.proof_of ths) Symtab.empty))
-      in
-          if null names orelse null deps then ()
-          else thm_deps_message (spaces_quote names, spaces_quote deps)
-      end
-  else ()
+  let
+    val valuethms = XML.Elem ("value", [("name", "thms")], [XML.Text thms]);
+    val valuedeps = XML.Elem ("value", [("name", "deps")], [XML.Text deps]);
+  in
+    issue_pgip (Metainforesponse
+      {attrs = [("infotype", "isabelle_theorem_dependencies")],
+       content = [valuethms, valuedeps]})
+  end;
 
 in
 
-fun setup_present_hook () =
-  ProofDisplay.add_hook (fn res => tell_thm_deps (maps #2 res));
+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 null names orelse null deps then ()
+      else thm_deps_message (spaces_quote names, spaces_quote deps)
+    end
+  else ());
 
 end;
 
+
 (** lexicalstructure element with keywords (PGIP version of elisp keywords file) **)
 
 fun lexicalstructure_keywords () =
@@ -1041,4 +1068,3 @@
 end
 
 end;
-