# HG changeset patch
# User wenzelm
# Date 1614445469 -3600
# Node ID df49ca5da9d037ef99b223624386230f14a114ea
# Parent  8664433956b349f96ef6cb41100efff0e870b184
clarified modules: more like ML;

diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_csdp.scala
--- a/src/Pure/Admin/build_csdp.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -124,8 +124,8 @@
 
       /* install */
 
-      File.copy(build_dir + Path.explode("LICENSE"), component_dir)
-      File.copy(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
+      Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
+      Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
 
       if (Platform.is_windows) {
         Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw,
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_e.scala
--- a/src/Pure/Admin/build_e.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_e.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -66,12 +66,13 @@
 
       /* install */
 
-      File.copy(build_dir + Path.basic("COPYING"), component_dir + Path.basic("LICENSE"))
+      Isabelle_System.copy_file(build_dir + Path.basic("COPYING"),
+        component_dir + Path.basic("LICENSE"))
 
       val install_files = List("epclextract", "eprover", "eprover-ho")
       for (name <- install_files ::: install_files.map(_ + ".exe")) {
         val path = build_dir + Path.basic("PROVER") + Path.basic(name)
-        if (path.is_file) File.copy(path, platform_dir)
+        if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
       }
       Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
         cwd = platform_dir.file).check
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_fonts.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -244,7 +244,7 @@
             progress.echo("Font " + target_file.toString + " ...")
 
             if (hinted) auto_hint(source_file, tmp_file)
-            else File.copy(source_file, tmp_file)
+            else Isabelle_System.copy_file(source_file, tmp_file)
 
             Fontforge.execute(
               Fontforge.commands(
@@ -328,7 +328,7 @@
 
 
     // README
-    File.copy(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
+    Isabelle_System.copy_file(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
   }
 
 
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -139,7 +139,7 @@
       val platform_dir = dir + platform.platform_path
       if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
 
-      File.move(jdk_dir, platform_dir)
+      Isabelle_System.move_file(jdk_dir, platform_dir)
 
       platform
     }
@@ -183,7 +183,9 @@
         File.write(Components.settings(component_dir), settings)
         File.write(component_dir + Path.explode("README"), readme(jdk_version))
 
-        for (platform <- platforms) File.move(dir + platform.platform_path, component_dir)
+        for (platform <- platforms) {
+          Isabelle_System.move_file(dir + platform.platform_path, component_dir)
+        }
 
         for (file <- File.find_files(component_dir.file, include_dirs = true)) {
           val path = file.toPath
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_polyml.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -112,13 +112,13 @@
     Isabelle_System.rm_tree(platform_dir)
     Isabelle_System.make_directory(platform_dir)
 
-    for (file <- sha1_files) File.copy(file, platform_dir)
+    for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir)
 
     for {
       d <- List("target/bin", "target/lib")
       dir = root + Path.explode(d)
       entry <- File.read_dir(dir)
-    } File.move(dir + Path.explode(entry), platform_dir)
+    } Isabelle_System.move_file(dir + Path.explode(entry), platform_dir)
 
     Executable.libraries_closure(
       platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs)
@@ -159,7 +159,7 @@
 
     val src_dir = component_dir + Path.explode("src")
     File.read_dir(component_dir) match {
-      case List(s) => File.move(component_dir + Path.basic(s), src_dir)
+      case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir)
       case _ => error("Source archive contains multiple directories")
     }
 
@@ -187,10 +187,10 @@
     Isabelle_System.new_directory(component_dir)
     extract_sources(source_archive, component_dir)
 
-    File.copy(Path.explode("~~/Admin/polyml/README"), component_dir)
+    Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir)
 
     val etc_dir = Isabelle_System.make_directory(component_dir + Path.explode("etc"))
-    File.copy(Path.explode("~~/Admin/polyml/settings"), etc_dir)
+    Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), etc_dir)
 
     sha1_root match {
       case Some(dir) =>
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_release.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -302,7 +302,7 @@
     File.set_executable(script_path, true)
 
     val component_dir = isabelle_target + Path.explode("contrib/Isabelle_app")
-    File.move(
+    Isabelle_System.move_file(
       component_dir + Path.explode(Platform.standard_platform(platform)) + Path.explode("Isabelle"),
       isabelle_target + Path.explode(isabelle_name))
     Isabelle_System.rm_tree(component_dir)
@@ -654,7 +654,7 @@
             val app_contents = isabelle_target + Path.explode("Contents")
 
             for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) {
-              File.copy(isabelle_target + Path.explode(icon),
+              Isabelle_System.copy_file(isabelle_target + Path.explode(icon),
                 Isabelle_System.make_directory(app_contents + Path.explode("Resources")))
             }
 
@@ -676,7 +676,8 @@
             progress.echo("Packaging " + archive_name + " ...")
 
             val isabelle_app = Path.explode(isabelle_name + ".app")
-            File.move(tmp_dir + Path.explode(isabelle_name), tmp_dir + isabelle_app)
+            Isabelle_System.move_file(tmp_dir + Path.explode(isabelle_name),
+              tmp_dir + isabelle_app)
 
             execute_tar(tmp_dir,
               "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
@@ -690,7 +691,7 @@
 
             // application launcher
 
-            File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+            Isabelle_System.move_file(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
 
             val app_template = Path.explode("~~/Admin/Windows/launch4j")
 
@@ -717,7 +718,7 @@
             execute(tmp_dir,
               "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
 
-            File.copy(app_template + Path.explode("manifest.xml"),
+            Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
               isabelle_target + isabelle_exe.ext("manifest"))
 
 
@@ -725,7 +726,8 @@
 
             val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
 
-            File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+            Isabelle_System.copy_file(cygwin_template + Path.explode("Cygwin-Terminal.bat"),
+              isabelle_target)
 
             val cygwin_mirror =
               File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
@@ -737,7 +739,7 @@
 
             for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
               val path = Path.explode(name)
-              File.copy(cygwin_template + path,
+              Isabelle_System.copy_file(cygwin_template + path,
                 isabelle_target + Path.explode("contrib/cygwin") + path)
             }
 
@@ -808,7 +810,7 @@
             List(List(isabelle_link)) ::: (if (afp_rev == "") Nil else List(List(afp_link))))))
 
       for ((bundle, _) <- website_platform_bundles)
-        File.copy(release.dist_dir + Path.explode(bundle), dir)
+        Isabelle_System.copy_file(release.dist_dir + Path.explode(bundle), dir)
     }
 
 
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_spass.scala
--- a/src/Pure/Admin/build_spass.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_spass.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -94,12 +94,13 @@
 
       /* install */
 
-      File.copy(build_dir + Path.basic("LICENCE"), component_dir + Path.basic("LICENSE"))
+      Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"),
+        component_dir + Path.basic("LICENSE"))
 
       val install_files = List("SPASS")
       for (name <- install_files ::: install_files.map(_ + ".exe")) {
         val path = build_dir + Path.basic(name)
-        if (path.is_file) File.copy(path, platform_dir)
+        if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
       }
 
 
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_sqlite.scala
--- a/src/Pure/Admin/build_sqlite.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_sqlite.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -73,7 +73,7 @@
 
       for ((file, dir) <- jar_files) {
         val target = Isabelle_System.make_directory(component_dir + Path.explode(dir))
-        File.copy(jar_dir + Path.explode(file), target)
+        Isabelle_System.copy_file(jar_dir + Path.explode(file), target)
       }
 
       File.set_executable(component_dir + Path.explode("x86_64-windows/sqlitejdbc.dll"), true)
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_vampire.scala
--- a/src/Pure/Admin/build_vampire.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_vampire.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -53,7 +53,7 @@
 
       val source_dir = tmp_dir + Path.explode("vampire")
 
-      File.copy(source_dir + Path.explode("LICENCE"), component_dir)
+      Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir)
 
 
       /* build versions */
@@ -79,7 +79,7 @@
 
         progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
 
-        File.copy(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+        Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
           platform_dir + Path.basic(exe).platform_exe)
       }
 
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_verit.scala
--- a/src/Pure/Admin/build_verit.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_verit.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -84,10 +84,10 @@
 
       /* install */
 
-      File.copy(build_dir + Path.explode("LICENSE"), component_dir)
+      Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir)
 
       val exe_path = Path.basic("veriT").platform_exe
-      File.copy(build_dir + exe_path, platform_dir)
+      Isabelle_System.copy_file(build_dir + exe_path, platform_dir)
       Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
 
 
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/build_zipperposition.scala
--- a/src/Pure/Admin/build_zipperposition.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -54,11 +54,12 @@
 
       /* install */
 
-      File.copy(build_dir + Path.explode("doc/zipperposition/LICENSE"), component_dir)
+      Isabelle_System.copy_file(build_dir + Path.explode("doc/zipperposition/LICENSE"),
+        component_dir)
 
       val prg_path = Path.basic("zipperposition")
       val exe_path = prg_path.platform_exe
-      File.copy(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
+      Isabelle_System.copy_file(build_dir + Path.basic("bin") + prg_path, platform_dir + exe_path)
 
       if (!Platform.is_windows) {
         Executable.libraries_closure(
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/components.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -72,7 +72,7 @@
       }
       for (dir <- copy_dir) {
         Isabelle_System.make_directory(dir)
-        File.copy(archive, dir)
+        Isabelle_System.copy_file(archive, dir)
       }
       unpack(target_dir getOrElse base_dir, archive, progress = progress)
     }
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Admin/other_isabelle.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -65,7 +65,7 @@
 
   def copy_fonts(target_dir: Path): Unit =
     Isabelle_Fonts.make_entries(getenv = getenv, hidden = true).
-      foreach(entry => File.copy(entry.path, target_dir))
+      foreach(entry => Isabelle_System.copy_file(entry.path, target_dir))
 
 
   /* components */
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/General/file.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -10,8 +10,8 @@
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
-import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
-  Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException}
+import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
+  FileVisitOption, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
@@ -265,13 +265,13 @@
 
   def write_backup(path: Path, text: CharSequence)
   {
-    if (path.is_file) move(path, path.backup)
+    if (path.is_file) Isabelle_System.move_file(path, path.backup)
     write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
-    if (path.is_file) move(path, path.backup2)
+    if (path.is_file) Isabelle_System.move_file(path, path.backup2)
     write(path, text)
   }
 
@@ -310,60 +310,6 @@
   def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
 
 
-  /* copy */
-
-  def copy(src: JFile, dst: JFile)
-  {
-    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
-    if (!eq(src, target))
-      Files.copy(src.toPath, target.toPath,
-        StandardCopyOption.COPY_ATTRIBUTES,
-        StandardCopyOption.REPLACE_EXISTING)
-  }
-
-  def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
-
-  def copy_base(base_dir: Path, src0: Path, target_dir: Path)
-  {
-    val src = src0.expand
-    val src_dir = src.dir
-    if (!src.starts_basic) error("Illegal path specification " + src + " beyond base directory")
-    copy(base_dir + src, Isabelle_System.make_directory(target_dir + src_dir))
-  }
-
-
-  /* move */
-
-  def move(src: JFile, dst: JFile)
-  {
-    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
-    if (!eq(src, target))
-      Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
-  }
-
-  def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
-
-
-  /* symbolic link */
-
-  def link(src: Path, dst: Path, force: Boolean = false)
-  {
-    val src_file = src.file
-    val dst_file = dst.file
-    val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
-
-    if (force) target.delete
-
-    try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
-    catch {
-      case _: UnsupportedOperationException if Platform.is_windows =>
-        Cygwin.link(standard_path(src), target)
-      case _: FileSystemException if Platform.is_windows =>
-        Cygwin.link(standard_path(src), target)
-    }
-  }
-
-
   /* permissions */
 
   def is_executable(path: Path): Boolean =
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/System/executable.scala
--- a/src/Pure/System/executable.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/System/executable.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -49,7 +49,7 @@
       }
 
     if (libs.nonEmpty) {
-      libs.foreach(lib => File.copy(Path.explode(lib), exe_dir))
+      libs.foreach(lib => Isabelle_System.copy_file(Path.explode(lib), exe_dir))
 
       if (Platform.is_linux) {
         if (patchelf) {
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -9,9 +9,11 @@
 
 
 import java.io.{File => JFile, IOException}
-import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
+import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
+  StandardCopyOption, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 
+
 import scala.annotation.tailrec
 
 
@@ -206,9 +208,65 @@
     if (path.is_dir) error("Directory already exists: " + path.absolute)
     else make_directory(path)
 
+
+
+  /* copy */
+
   def copy_dir(dir1: Path, dir2: Path): Unit =
     bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)).check
 
+  def copy_file(src: JFile, dst: JFile): Unit =
+  {
+    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+    if (!eq(src, target)) {
+      Files.copy(src.toPath, target.toPath,
+        StandardCopyOption.COPY_ATTRIBUTES,
+        StandardCopyOption.REPLACE_EXISTING)
+    }
+  }
+
+  def copy_file(path1: Path, path2: Path): Unit = copy_file(path1.file, path2.file)
+
+  def copy_file_base(base_dir: Path, src0: Path, target_dir: Path): Unit =
+  {
+    val src = src0.expand
+    val src_dir = src.dir
+    if (!src.starts_basic) error("Illegal path specification " + src + " beyond base directory")
+    copy_file(base_dir + src, Isabelle_System.make_directory(target_dir + src_dir))
+  }
+
+
+  /* move */
+
+  def move_file(src: JFile, dst: JFile)
+  {
+    val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
+    if (!eq(src, target))
+      Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
+  }
+
+  def move_file(path1: Path, path2: Path): Unit = move_file(path1.file, path2.file)
+
+
+  /* symbolic link */
+
+  def symlink(src: Path, dst: Path, force: Boolean = false)
+  {
+    val src_file = src.file
+    val dst_file = dst.file
+    val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
+
+    if (force) target.delete
+
+    try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
+    catch {
+      case _: UnsupportedOperationException if Platform.is_windows =>
+        Cygwin.link(File.standard_path(src), target)
+      case _: FileSystemException if Platform.is_windows =>
+        Cygwin.link(File.standard_path(src), target)
+    }
+  }
+
 
   /* tmp files */
 
@@ -291,8 +349,8 @@
 
     f(new_dir)
 
-    if (dir.is_dir) File.move(dir, old_dir)
-    File.move(new_dir, dir)
+    if (dir.is_dir) move_file(dir, old_dir)
+    move_file(new_dir, dir)
     rm_tree(old_dir)
   }
 
@@ -445,7 +503,7 @@
   {
     args.find(_ != "") match {
       case Some(logic) => logic
-      case None => Isabelle_System.getenv_strict("ISABELLE_LOGIC")
+      case None => getenv_strict("ISABELLE_LOGIC")
     }
   }
 }
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Thy/bibtex.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -655,7 +655,7 @@
       }
 
       for ((a, b) <- bib_files zip bib_names) {
-        File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
+        Isabelle_System.copy_file(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib"))
       }
 
 
@@ -668,7 +668,7 @@
             error("Bad style for bibtex HTML output: " + quote(style) +
               "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")")
         }
-      File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
+      Isabelle_System.copy_file(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir)
 
 
       /* result */
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -27,7 +27,7 @@
     {
       val fonts_dir = Isabelle_System.make_directory(dir + fonts_path)
       for (entry <- Isabelle_Fonts.fonts(hidden = true))
-        File.copy(entry.path, fonts_dir)
+        Isabelle_System.copy_file(entry.path, fonts_dir)
     }
 
     def head(title: String, rest: XML.Body = Nil): XML.Tree =
@@ -364,7 +364,7 @@
   {
     if (!(browser_info + Path.explode("index.html")).is_file) {
       Isabelle_System.make_directory(browser_info)
-      File.copy(Path.explode("~~/lib/logo/isabelle.gif"),
+      Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle.gif"),
         browser_info + Path.explode("isabelle.gif"))
       File.write(browser_info + Path.explode("index.html"),
         File.read(Path.explode("~~/lib/html/library_index_header.template")) +
@@ -433,7 +433,7 @@
 
       val readme_links =
         if ((info.dir + readme_path).is_file) {
-          File.copy(info.dir + readme_path, session_dir + readme_path)
+          Isabelle_System.copy_file(info.dir + readme_path, session_dir + readme_path)
           List(HTML.link(readme_path, HTML.text("README")))
         }
         else Nil
@@ -582,7 +582,9 @@
 
       Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check
       File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty)
-      for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir)
+      for ((base_dir, src) <- info.document_files) {
+        Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir)
+      }
 
       File.write(doc_dir + session_tex_path,
         Library.terminate_lines(
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Tools/build_docker.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -86,7 +86,8 @@
             if (!Url.is_readable(app_archive))
               error("Cannot access remote archive " + app_archive)
           }
-          else File.copy(Path.explode(app_archive), tmp_dir + Path.explode("Isabelle.tar.gz"))
+          else Isabelle_System.copy_file(Path.explode(app_archive),
+            tmp_dir + Path.explode("Isabelle.tar.gz"))
 
           val quiet_option = if (verbose) "" else " -q"
           val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
diff -r 8664433956b3 -r df49ca5da9d0 src/Pure/Tools/scala_project.scala
--- a/src/Pure/Tools/scala_project.scala	Sat Feb 27 17:33:40 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala	Sat Feb 27 18:04:29 2021 +0100
@@ -129,7 +129,8 @@
         }).getOrElse(error("Unknown directory prefix for " + quote(file)))
 
       Isabelle_System.make_directory(target)
-      if (symlinks) File.link(path, target) else File.copy(path, target)
+      if (symlinks) Isabelle_System.symlink(path, target)
+      else Isabelle_System.copy_file(path, target)
     }
 
     val jars =