theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
authorwenzelm
Tue Sep 02 22:20:25 2008 +0200 (2008-09-02)
changeset 28096046418f64474
parent 28095 7eaf0813bdc3
child 28097 003dff7410c1
theorem dependency output: Toplevel.add_hook, ProofGeneralPgip.new_thms_deps;
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 02 22:20:24 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Sep 02 22:20:25 2008 +0200
     1.3 @@ -173,22 +173,15 @@
     1.4  fun thm_deps_message (thms, deps) =
     1.5    emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
     1.6  
     1.7 -fun tell_thm_deps ths =
     1.8 -  if print_mode_active thm_depsN then
     1.9 -    let
    1.10 -      val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
    1.11 -      val deps = Symtab.keys (fold Proofterm.thms_of_proof'
    1.12 -                                   (map Thm.proof_of ths) Symtab.empty);
    1.13 -    in
    1.14 +in
    1.15 +
    1.16 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
    1.17 +  if print_mode_active thm_depsN andalso Toplevel.is_theory state' andalso is_none opt_err then
    1.18 +    let val (names, deps) = ProofGeneralPgip.new_thms_deps state state' in
    1.19        if null names orelse null deps then ()
    1.20        else thm_deps_message (spaces_quote names, spaces_quote deps)
    1.21      end
    1.22 -  else ();
    1.23 -
    1.24 -in
    1.25 -
    1.26 -fun setup_present_hook () =
    1.27 -  ProofDisplay.add_hook (fn res => tell_thm_deps (maps #2 res));
    1.28 +  else ());
    1.29  
    1.30  end;
    1.31