# HG changeset patch
# User wenzelm
# Date 1030439067 -7200
# Node ID 9269275e5da682e5ca5ae531064d879428078025
# Parent  cafd1f98d65868c07e7eb1a6293cdfc532561aeb
result dependency output;

diff -r cafd1f98d658 -r 9269275e5da6 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue Aug 27 11:04:00 2002 +0200
+++ b/src/Pure/proof_general.ML	Tue Aug 27 11:04:27 2002 +0200
@@ -114,9 +114,9 @@
   if pgml () then writeln_default (XML.element kind [] [prefix_lines prfx s])
   else decorated_output bg en prfx s;
 
-val notify = message "notify" (oct_char "360") (oct_char "361") "";
+in
 
-in
+val notify = message "notify" (oct_char "360") (oct_char "361") "";
 
 fun setup_messages () =
  (writeln_fn := message "output" "" "" "";
@@ -160,6 +160,30 @@
 end;
 
 
+(* result dependency output *)
+
+local
+
+fun tell_thm_deps ths =
+  let
+    val names = map Thm.name_of_thm ths;
+    val refs =
+      foldl (uncurry Proofterm.thms_of_proof) (Symtab.empty, map Thm.proof_of ths)
+      |> Symtab.keys;
+    val deps = refs \\ names \ "";
+  in
+    if null deps then ()
+    else notify ("Proof General, result dependencies are: " ^ space_implode " " (map quote deps))
+  end;
+
+in
+
+fun setup_present_hook () =
+  Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
+
+end;
+
+
 (* theory loader actions *)
 
 local
@@ -311,6 +335,7 @@
     setup_messages ();
     setup_state ();
     setup_thy_loader ();
+    setup_present_hook ();
     set initialized; ()));
   sync_thy_loader ();
   print_mode := proof_generalN :: (! print_mode \ proof_generalN);