more operations;
authorwenzelm
Fri, 30 Jun 2017 14:17:48 +0200
changeset 66233 7188967253e5
parent 66232 be0ab4b94c62
child 66234 836898197296
more operations;
src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Jun 30 14:01:55 2017 +0200
+++ b/src/Pure/General/file.scala	Fri Jun 30 14:17:48 2017 +0200
@@ -97,7 +97,10 @@
   /* platform files */
 
   def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
+  def absolute_name(file: JFile): String = absolute(file).getPath
+
   def canonical(file: JFile): JFile = file.getCanonicalFile
+  def canonical_name(file: JFile): String = canonical(file).getPath
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def pwd(): Path = path(Path.current.absolute_file)