# HG changeset patch
# User wenzelm
# Date 1498825068 -7200
# Node ID 7188967253e57a7b09d1359da273278e50b849f3
# Parent  be0ab4b94c6214223c0c1c81581b1a98ad6fab65
more operations;

diff -r be0ab4b94c62 -r 7188967253e5 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)