# HG changeset patch
# User wenzelm
# Date 1498824115 -7200
# Node ID be0ab4b94c6214223c0c1c81581b1a98ad6fab65
# Parent  406b5ae7f5f3661ff754ddfcaaeff93156db60be
clarified signature;

diff -r 406b5ae7f5f3 -r be0ab4b94c62 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Jun 30 13:21:47 2017 +0200
+++ b/src/Pure/General/file.scala	Fri Jun 30 14:01:55 2017 +0200
@@ -47,9 +47,6 @@
 
   def standard_path(file: JFile): String = standard_path(file.getPath)
 
-  def path(file: JFile): Path = Path.explode(standard_path(file))
-  def pwd(): Path = path(Path.current.file.toPath.toAbsolutePath.toFile)
-
   def standard_url(name: String): String =
     try {
       val url = new URL(name)
@@ -97,6 +94,15 @@
   def platform_file(path: Path): JFile = new JFile(platform_path(path))
 
 
+  /* platform files */
+
+  def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
+  def canonical(file: JFile): JFile = file.getCanonicalFile
+
+  def path(file: JFile): Path = Path.explode(standard_path(file))
+  def pwd(): Path = path(Path.current.absolute_file)
+
+
   /* bash path */
 
   def bash_path(path: Path): String = Bash.string(standard_path(path))
diff -r 406b5ae7f5f3 -r be0ab4b94c62 src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Fri Jun 30 13:21:47 2017 +0200
+++ b/src/Pure/General/path.scala	Fri Jun 30 14:01:55 2017 +0200
@@ -207,11 +207,12 @@
   def position: Position.T = Position.File(implode)
 
 
-  /* platform file */
+  /* platform files */
 
   def file: JFile = File.platform_file(this)
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
-  def canonical_file: JFile = file.getCanonicalFile
+  def absolute_file: JFile = File.absolute(file)
+  def canonical_file: JFile = File.canonical(file)
 }