theorem dependency hook: check previous state;
authorwenzelm
Wed Sep 03 11:27:15 2008 +0200 (2008-09-03)
changeset 2810648b9c8756020
parent 28105 44054657ea56
child 28107 760ecc6fc1bd
theorem dependency hook: check previous state;
src/Pure/ProofGeneral/proof_general_emacs.ML
     1.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 11:26:59 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 11:27:15 2008 +0200
     1.3 @@ -176,7 +176,9 @@
     1.4  in
     1.5  
     1.6  fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
     1.7 -  if print_mode_active thm_depsN andalso Toplevel.is_theory state' then
     1.8 +  if print_mode_active thm_depsN andalso
     1.9 +    can Toplevel.theory_of state andalso Toplevel.is_theory state'
    1.10 +  then
    1.11      let val (names, deps) =
    1.12        ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
    1.13      in