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.
ThyInfo.register_thy;
authorwenzelm
Tue, 31 Jul 2007 00:56:32 +0200
changeset 24079 3ba5d68e076b
parent 24078 04b28c723d43
child 24080 8c67d869531b
ThyInfo.register_thy;
src/Pure/ProofGeneral/proof_general_emacs.ML file | annotate | diff | comparison | revisions
src/Pure/ProofGeneral/proof_general_pgip.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 31 00:56:31 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 31 00:56:32 2007 +0200
@@ -169,7 +169,7 @@
   let val name = thy_name file in
     if ThyInfo.known_thy name then
      (ThyInfo.touch_child_thys name;
-      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
+      ThyInfo.register_thy name handle ERROR msg =>
        (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
         tell_file_retracted (Path.base (Path.explode file))))
     else raise Toplevel.UNDEF
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 31 00:56:31 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 31 00:56:32 2007 +0200
@@ -356,7 +356,7 @@
   let val name = thy_name path in
     if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
      (ThyInfo.touch_child_thys name;
-      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
+      ThyInfo.register_thy name handle ERROR msg =>
        (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
         tell_file_retracted true (Path.base path)))
     else raise Toplevel.UNDEF
isabelle