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