proper_inform_file_processed: Isar.init_point starts fresh command sequence;
authorwenzelm
Thu, 10 Jul 2008 21:03:47 +0200
changeset 27536 1dcb8a6bdfe9
parent 27535 518380d43585
child 27537 17838612217b
proper_inform_file_processed: Isar.init_point starts fresh command sequence;
src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Jul 10 20:54:00 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Jul 10 21:03:47 2008 +0200
@@ -148,6 +148,7 @@
     val _ = ThyInfo.register_thy name handle ERROR msg =>
       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
         tell_file_retracted (thy_path file));
+    val _ = Isar.init_point ();
   in () end;
 
 fun vacuous_inform_file_processed file () = tell_file_retracted (thy_path file);