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))))]