--- a/src/Pure/proof_general.ML Fri Nov 24 16:38:42 2006 +0100
+++ b/src/Pure/proof_general.ML Fri Nov 24 17:22:32 2006 +0100
@@ -264,7 +264,7 @@
val thyname_attr = pair "thyname";
val url_attr = pair "url";
- fun localfile_url_attr abspath = url_attr ("file://" ^ abspath);
+ fun localfile_url_attr abspath = url_attr ("file:" ^ abspath);
in
fun setup_messages () =
@@ -314,16 +314,20 @@
fun tell_file_loaded path =
if pgip () then
issue_pgipe "informfileloaded"
- [localfile_url_attr (XML.text (File.platform_path path))]
+ [localfile_url_attr (XML.text (File.platform_path
+ (File.full_path path)))]
else
- emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
+ emacs_notify ("Proof General, this file is loaded: " ^
+ quote (File.platform_path path));
fun tell_file_retracted path =
if pgip() then
issue_pgipe "informfileretracted"
- [localfile_url_attr (XML.text (File.platform_path path))]
+ [localfile_url_attr (XML.text (File.platform_path
+ (File.full_path path)))]
else
- emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
+ emacs_notify ("Proof General, you can unlock the file "
+ ^ quote (File.platform_path path));
(* theory / proof state output *)