thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
authorwenzelm
Thu, 15 Nov 2007 11:49:04 +0100
changeset 25436 ca46d8a66b69
parent 25435 bafaea364a66
child 25437 1170e384764d
thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin);
src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 15 11:49:03 2007 +0100
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Nov 15 11:49:04 2007 +0100
@@ -166,7 +166,7 @@
 
 (* get informed about files *)
 
-val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
+val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
 
 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;