# HG changeset patch
# User wenzelm
# Date 1625744052 -7200
# Node ID e61add9d5b5e31752e5e3d078014994c14c57f74
# Parent  3cee9d20308e9f285432773afc171530d3fc322d
tuned signature;

diff -r 3cee9d20308e -r e61add9d5b5e src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -58,7 +58,7 @@
             Bash.string(backup + "/log/.") + " " + File.bash_path(main_dir) + "/log/.").check
 
         if (!Isabelle_Devel.cronjob_log.is_file)
-          Files.createSymbolicLink(Isabelle_Devel.cronjob_log.file.toPath, current_log.file.toPath)
+          Files.createSymbolicLink(Isabelle_Devel.cronjob_log.java_path, current_log.java_path)
       })
 
   val exit: Logger_Task =
diff -r 3cee9d20308e -r e61add9d5b5e src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/General/file.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -68,8 +68,8 @@
 
   def relative_path(base: Path, other: Path): Option[Path] =
   {
-    val base_path = base.file.toPath
-    val other_path = other.file.toPath
+    val base_path = base.java_path
+    val other_path = other.java_path
     if (other_path.startsWith(base_path))
       Some(path(base_path.relativize(other_path).toFile))
     else None
diff -r 3cee9d20308e -r e61add9d5b5e src/Pure/General/path.scala
--- a/src/Pure/General/path.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/General/path.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -10,6 +10,7 @@
 
 import java.util.{Map => JMap}
 import java.io.{File => JFile}
+import java.nio.file.{Path => JPath}
 
 import scala.util.matching.Regex
 
@@ -306,6 +307,8 @@
   def is_file: Boolean = file.isFile
   def is_dir: Boolean = file.isDirectory
 
+  def java_path: JPath = file.toPath
+
   def absolute_file: JFile = File.absolute(file)
   def canonical_file: JFile = File.canonical(file)
 
diff -r 3cee9d20308e -r e61add9d5b5e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -153,7 +153,7 @@
   def make_directory(path: Path): Path =
   {
     if (!path.is_dir) {
-      try { Files.createDirectories(path.file.toPath) }
+      try { Files.createDirectories(path.java_path) }
       catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) }
     }
     path
diff -r 3cee9d20308e -r e61add9d5b5e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Jul 08 13:16:31 2021 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Jul 08 13:34:12 2021 +0200
@@ -1144,7 +1144,7 @@
   def read_heap_digest(heap: Path): Option[String] =
   {
     if (heap.is_file) {
-      using(FileChannel.open(heap.file.toPath, StandardOpenOption.READ))(file =>
+      using(FileChannel.open(heap.java_path, StandardOpenOption.READ))(file =>
       {
         val len = file.size
         val n = sha1_prefix.length + SHA1.digest_length