# HG changeset patch # User wenzelm # Date 1669840566 -3600 # Node ID 88cecb9f1cdc3e6771eb063857fadd4b11eb5027 # Parent cee207c2ddecf73c3d7e55f86059b01ee9c0df27 proper unzip with strip option, within the JVM; tuned component build process; diff -r cee207c2ddec -r 88cecb9f1cdc src/Pure/Admin/build_easychair.scala --- 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 */ diff -r cee207c2ddec -r 88cecb9f1cdc src/Pure/Admin/build_foiltex.scala --- 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 + """ diff -r cee207c2ddec -r 88cecb9f1cdc src/Pure/Admin/build_llncs.scala --- 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 + """ diff -r cee207c2ddec -r 88cecb9f1cdc src/Pure/General/file.scala --- 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 diff -r cee207c2ddec -r 88cecb9f1cdc src/Pure/System/isabelle_system.scala --- 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 " diff -r cee207c2ddec -r 88cecb9f1cdc src/Tools/VSCode/src/build_vscodium.scala --- 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") - } }