src/Pure/General/url.scala
changeset 66235 d4fa51e7c4ff
parent 66234 836898197296
child 67245 caa4c9001009
--- a/src/Pure/General/url.scala	Fri Jun 30 14:19:37 2017 +0200
+++ b/src/Pure/General/url.scala	Fri Jun 30 14:26:45 2017 +0200
@@ -61,6 +61,9 @@
         false
     }
 
+  def absolute_file(uri: String): JFile = File.absolute(parse_file(uri))
+  def absolute_file_name(uri: String): String = absolute_file(uri).getPath
+
   def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 }