# HG changeset patch # User wenzelm # Date 1195123744 -3600 # Node ID ca46d8a66b693ae0d58188e87c7926e6ba42b296 # Parent bafaea364a66a837cfe14cca124e244fea4fe8b0 thy_name: be very liberal about file name format (workaround problem with XEmacs on cygwin); diff -r bafaea364a66 -r ca46d8a66b69 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;