# 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;