# HG changeset patch
# User wenzelm
# Date 1216058233 -7200
# Node ID 2234ace5b538b8c2e7eca3b0eadd8e93f5c9aad1
# Parent  e0cd0396945aa8ae4da37635405a50ad8979e9ef
inform_file_processed: try harder not to fail, ensure

diff -r e0cd0396945a -r 2234ace5b538 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 19:57:11 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Jul 14 19:57:13 2008 +0200
@@ -137,17 +137,16 @@
 
 fun inform_file_processed file =
   let
+    val _ = Isar.init_point ();
     val name = thy_name file;
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
       if ThyInfo.check_known_thy name then
-        (Isar.commit_exit ();
-          ThyInfo.touch_child_thys name;
-          ThyInfo.register_thy name handle ERROR msg =>
+        (Isar.commit_exit (); ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
+          handle ERROR msg =>
             (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
-             tell_file_retracted (ThyLoad.thy_path name)))
+              tell_file_retracted (ThyLoad.thy_path name))
       else ();
-    val _ = Isar.init_point ();
   in () end;