# HG changeset patch
# User wenzelm
# Date 1215716627 -7200
# Node ID 1dcb8a6bdfe994037b98151784cfa4274dc705f8
# Parent  518380d435856ed9b99bd6521ffcba70c65fa29c
proper_inform_file_processed: Isar.init_point starts fresh command sequence;

diff -r 518380d43585 -r 1dcb8a6bdfe9 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);