# HG changeset patch
# User aspinall
# Date 1164385352 -3600
# Node ID e7dcae358d1a25c87938ad5b1d0bf12ca3e6cb22
# Parent  9e9fff87dc6c05670d1aaf3564304b61f7b96ddd
Send full paths in PGIP version of file loaded/retracted messages

diff -r 9e9fff87dc6c -r e7dcae358d1a src/Pure/proof_general.ML
--- 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 *)