# HG changeset patch
# User aspinall
# Date 1167936780 -3600
# Node ID 34e190b243993db890a656ba3898a7ca53c1f817
# Parent  5c60e46a07c1171e5558d96ff456d853db86076d
Be more chatty in PGIP file operations.proof_general_pgip.ML

diff -r 5c60e46a07c1 -r 34e190b24399 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Thu Jan 04 19:27:08 2007 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Thu Jan 04 19:53:00 2007 +0100
@@ -96,6 +96,7 @@
     val pgipurl_of_string : string -> pgipurl	       (* raises PGIP *)
     val pgipurl_of_path : Path.T -> pgipurl
     val path_of_pgipurl : pgipurl -> Path.T
+    val string_of_pgipurl : pgipurl -> string
     val attrs_of_pgipurl : pgipurl -> XML.attributes
     val pgipurl_of_attrs : XML.attributes -> pgipurl   (* raises PGIP *)
 
@@ -352,6 +353,8 @@
 
 fun path_of_pgipurl p = p  (* potentially raises PGIP, but not with this implementation *)
 
+fun string_of_pgipurl p = Path.implode p
+
 fun attrs_of_pgipurl purl = 
     [("url", "file:" ^ (XML.text (File.platform_path (File.full_path purl))))]