# HG changeset patch
# User wenzelm
# Date 1195466949 -3600
# Node ID 1af14e8f225bfed2c167b7045b6edf369e69bc21
# Parent  0337e3df3187a483035e66d7f5bc20b181e42e9b
inform_file_processed: made even more robust against bad file specs;

diff -r 0337e3df3187 -r 1af14e8f225b src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Nov 18 16:10:12 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Nov 19 11:09:09 2007 +0100
@@ -174,7 +174,8 @@
 
 in
 
-val check_thy = ThyInfo.check_known_thy o thy_name;
+fun check_thy "" = false
+  | check_thy file = ThyInfo.check_known_thy (thy_name file);
 
 fun proper_inform_file_processed file () =
   let
@@ -252,7 +253,8 @@
 fun inform_file_processedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.init_empty (K true) (vacuous_inform_file_processed file) o
+      Toplevel.imperative (fn () => error "Bad file name") o
+      Toplevel.init_empty (fn _ => file <> "") (vacuous_inform_file_processed file) o
       Toplevel.kill o
       Toplevel.init_empty (fn _ => check_thy file) (proper_inform_file_processed file)));