Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
theorem dependency hook: check previous state;
authorwenzelm
Wed, 03 Sep 2008 11:27:15 +0200
changeset 28106 48b9c8756020
parent 28105 44054657ea56
child 28107 760ecc6fc1bd
theorem dependency hook: check previous state;
src/Pure/ProofGeneral/proof_general_emacs.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 11:26:59 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Wed Sep 03 11:27:15 2008 +0200
@@ -176,7 +176,9 @@
 in
 
 fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
-  if print_mode_active thm_depsN andalso Toplevel.is_theory state' then
+  if print_mode_active thm_depsN andalso
+    can Toplevel.theory_of state andalso Toplevel.is_theory state'
+  then
     let val (names, deps) =
       ProofGeneralPgip.new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state')
     in
isabelle