# HG changeset patch
# User wenzelm
# Date 1476473692 -7200
# Node ID 284e8ca54c211c9d254ddce8ab27a4536d4b7595
# Parent  b265dd04d57d3a065c3e1be5ce7fa6d93321fb2b
more operations;

diff -r b265dd04d57d -r 284e8ca54c21 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Oct 14 20:53:10 2016 +0200
+++ b/src/Pure/General/file.scala	Fri Oct 14 21:34:52 2016 +0200
@@ -56,6 +56,8 @@
     }
     catch { case _: MalformedURLException => standard_path(name) }
 
+  def path(file: JFile): Path = Path.explode(standard_path(file.getAbsolutePath))
+
 
   /* platform path (Windows or Posix) */