src/Pure/ProofGeneral/proof_general_emacs.ML
changeset 25436 ca46d8a66b69
parent 25192 b568f8c5d5ca
child 25442 0337e3df3187
equal deleted inserted replaced
25435:bafaea364a66 25436:ca46d8a66b69
   164 end;
   164 end;
   165 
   165 
   166 
   166 
   167 (* get informed about files *)
   167 (* get informed about files *)
   168 
   168 
   169 val thy_name = Path.implode o #1 o Path.split_ext o Path.base o Path.explode;
   169 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
   170 
   170 
   171 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   171 val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   172 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   172 val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   173 
   173 
   174 fun proper_inform_file_processed file () =
   174 fun proper_inform_file_processed file () =