--- 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,
--- 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
--- 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)
}
--- 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
--- 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) =>
--- 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)
}
--- 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)
}
--- 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)
--- 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)
}
--- 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)
--- 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(
--- 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)
}
--- 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 */
--- 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 =
--- 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) {
--- 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")
}
}
}
--- 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 */
--- 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(
--- 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)
--- 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 =