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 }