clarified file operations;

--- a/src/Pure/Admin/build_history.scala	Fri Oct 14 20:07:22 2016 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri Oct 14 20:53:10 2016 +0200
@@ -119,7 +119,7 @@
   {
     /* sanity checks */
 
-    if (File.eq(Path.explode("~~").file, hg.root.file))
+    if (File.eq(Path.explode("~~"), hg.root))
       error("Repository coincides with ISABELLE_HOME=" + Path.explode("~~").expand)
 
     for (threads <- threads_list if threads < 1) error("Bad threads value < 1: " + threads)
@@ -170,10 +170,10 @@
             "bin/isabelle jedit -b" + (if (fresh) " -f" else ""),
           redirect = true, echo = verbose).check
 
-        Isabelle_System.rm_tree(isabelle_base_log.file)
+        Isabelle_System.rm_tree(isabelle_base_log)
       }
 
-      Isabelle_System.rm_tree(isabelle_output.file)
+      Isabelle_System.rm_tree(isabelle_output)
       Isabelle_System.mkdirs(isabelle_output)
 
 

--- a/src/Pure/General/file.scala	Fri Oct 14 20:07:22 2016 +0200
+++ b/src/Pure/General/file.scala	Fri Oct 14 20:53:10 2016 +0200
@@ -243,13 +243,13 @@
 
   def write_backup(path: Path, text: CharSequence)
   {
-    path.file renameTo path.backup.file
+    mv(path, path.backup)
     write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
-    path.file renameTo path.backup2.file
+    mv(path, path.backup2)
     write(path, text)
   }
 
@@ -263,12 +263,17 @@
   def append(path: Path, text: CharSequence): Unit = append(path.file, text)
 
 
-  /* copy */
+  /* eq */
 
   def eq(file1: JFile, file2: JFile): Boolean =
     try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
     catch { case ERROR(_) => false }
 
+  def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
+
+
+  /* copy */
+
   def copy(src: JFile, dst: JFile)
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
@@ -279,4 +284,12 @@
   }
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
+
+
+  /* move */
+
+  def mv(file1: JFile, file2: JFile): Unit =
+    Files.move(file1.toPath, file2.toPath, StandardCopyOption.REPLACE_EXISTING)
+
+  def mv(path1: Path, path2: Path): Unit = mv(path1.file, path2.file)
 }

--- a/src/Pure/System/isabelle_system.scala	Fri Oct 14 20:07:22 2016 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Oct 14 20:53:10 2016 +0200
@@ -211,6 +211,8 @@
 
   /* tmp dirs */
 
+  def rm_tree(root: Path): Unit = rm_tree(root.file)
+
   def rm_tree(root: JFile)
   {
     root.delete