--- a/src/Pure/Admin/build_easychair.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala Wed Nov 30 21:36:06 2022 +0100
@@ -40,9 +40,7 @@
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(easychair_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
--- a/src/Pure/Admin/build_foiltex.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala Wed Nov 30 21:36:06 2022 +0100
@@ -29,29 +29,25 @@
val foiltex_dir = File.get_dir(download_dir, title = download_url)
- val README = Path.explode("README")
- val README_flt = Path.explode("README.flt")
- Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt)
-
- Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check
-
/* component */
+ val README = Path.explode("README")
val version = {
val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
- split_lines(File.read(foiltex_dir + README_flt))
+ split_lines(File.read(foiltex_dir + README))
.collectFirst({ case Version(v) => v })
- .getOrElse(error("Failed to detect version in " + README_flt))
+ .getOrElse(error("Failed to detect version in " + README))
}
val component = "foiltex-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(foiltex_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
+
+ Isabelle_System.bash("pdflatex foiltex.ins", cwd = component_dir.path.file).check
+ (component_dir.path + Path.basic("foiltex.log")).file.delete()
/* settings */
@@ -65,6 +61,9 @@
/* README */
+ Isabelle_System.move_file(component_dir.README,
+ component_dir.path + Path.basic("README.flt"))
+
File.write(component_dir.README,
"""This is FoilTeX from
""" + download_url + """
--- a/src/Pure/Admin/build_llncs.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala Wed Nov 30 21:36:06 2022 +0100
@@ -32,26 +32,22 @@
val llncs_dir = File.get_dir(download_dir, title = download_url)
- val readme = Path.explode("README.md")
- File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
-
/* component */
+ val README_md = Path.explode("README.md")
val version = {
val Version = """^_.* v(.*)_$""".r
- split_lines(File.read(llncs_dir + readme))
+ split_lines(File.read(llncs_dir + README_md))
.collectFirst({ case Version(v) => v })
- .getOrElse(error("Failed to detect version in " + readme))
+ .getOrElse(error("Failed to detect version in " + README_md))
}
val component = "llncs-" + version
val component_dir =
Components.Directory.create(target_dir + Path.basic(component), progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(llncs_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
@@ -65,6 +61,8 @@
/* README */
+ File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0"))
+
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
""" + download_url + """
--- a/src/Pure/General/file.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/General/file.scala Wed Nov 30 21:36:06 2022 +0100
@@ -61,6 +61,8 @@
def canonical_name(file: JFile): String = canonical(file).getPath
def path(file: JFile): Path = Path.explode(standard_path(file))
+ def path(java_path: JPath): Path = path(java_path.toFile)
+
def pwd(): Path = path(Path.current.absolute_file)
def uri(file: JFile): URI = file.toURI
--- a/src/Pure/System/isabelle_system.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala Wed Nov 30 21:36:06 2022 +0100
@@ -8,12 +8,15 @@
import java.util.{Map => JMap, HashMap}
+import java.util.zip.ZipFile
import java.io.{File => JFile, IOException}
import java.net.ServerSocket
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
+import scala.jdk.CollectionConverters._
+
object Isabelle_System {
/* settings environment */
@@ -436,14 +439,34 @@
def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = {
val name = archive.file_name
make_directory(dir)
- if (File.is_zip(name)) {
- require(!strip, "Cannot extract/strip zip archive")
- Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check
- }
- else if (File.is_jar(name)) {
- require(!strip, "Cannot extract/strip jar archive")
- Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_platform_path(archive.absolute),
- cwd = dir.file).check
+ if (File.is_zip(name) || File.is_jar(name)) {
+ using(new ZipFile(archive.file)) { zip_file =>
+ val items =
+ for (entry <- zip_file.entries().asScala.toList)
+ yield {
+ val input = JPath.of(entry.getName)
+ val count = input.getNameCount
+ val output =
+ if (strip && count <= 1) None
+ else if (strip) Some(input.subpath(1, count))
+ else Some(input)
+ val result = output.map(dir.java_path.resolve(_))
+ for (res <- result) {
+ if (entry.isDirectory) Files.createDirectories(res)
+ else {
+ val bytes = using(zip_file.getInputStream(entry))(Bytes.read_stream(_))
+ Files.createDirectories(res.getParent)
+ Files.write(res, bytes.array)
+ }
+ }
+ (entry, result)
+ }
+ for {
+ (entry, Some(res)) <- items
+ if !entry.isDirectory
+ t <- Option(entry.getLastModifiedTime)
+ } Files.setLastModifiedTime(res, t)
+ }
}
else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) {
val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf "
--- a/src/Tools/VSCode/src/build_vscodium.scala Wed Nov 30 15:53:21 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala Wed Nov 30 21:36:06 2022 +0100
@@ -66,7 +66,6 @@
def is_linux: Boolean = platform == Platform.Family.linux
def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
- def download_zip: Boolean = File.is_zip(download_name)
def download(dir: Path, progress: Progress = new Progress): Unit = {
Isabelle_System.with_tmp_file("download") { download_file =>
@@ -270,10 +269,6 @@
if (platforms.contains(Platform.Family.windows)) {
Isabelle_System.require_command("wine")
}
-
- if (platforms.exists(platform => the_platform_info(platform).download_zip)) {
- Isabelle_System.require_command("unzip", test = "-h")
- }
}