--- a/src/Pure/Admin/build_release.scala Fri Apr 01 11:51:42 2022 +0200
+++ b/src/Pure/Admin/build_release.scala Fri Apr 01 17:06:10 2022 +0200
@@ -7,8 +7,7 @@
package isabelle
-object Build_Release
-{
+object Build_Release {
/** release context **/
private def execute(dir: Path, script: String): Unit =
@@ -20,14 +19,13 @@
private def bash_java_opens(args: String*): String =
Bash.strings(args.toList.flatMap(arg => List("--add-opens", arg + "=ALL-UNNAMED")))
- object Release_Context
- {
+ object Release_Context {
def apply(
target_dir: Path,
release_name: String = "",
components_base: Path = Components.default_components_base,
- progress: Progress = new Progress): Release_Context =
- {
+ progress: Progress = new Progress
+ ): Release_Context = {
val date = Date.now()
val dist_name = proper_string(release_name) getOrElse ("Isabelle_" + Date.Format.date(date))
val dist_dir = (target_dir + Path.explode("dist-" + dist_name)).absolute
@@ -40,8 +38,8 @@
val dist_name: String,
val dist_dir: Path,
val components_base: Path,
- val progress: Progress)
- {
+ val progress: Progress
+ ) {
override def toString: String = dist_name
val isabelle: Path = Path.explode(dist_name)
@@ -54,8 +52,7 @@
isabelle_identifier = dist_name + "-build",
progress = progress)
- def make_announce(id: String): Unit =
- {
+ def make_announce(id: String): Unit = {
if (release_name.isEmpty) {
File.write(isabelle_dir + Path.explode("ANNOUNCE"),
"""
@@ -67,8 +64,7 @@
}
}
- def make_contrib(): Unit =
- {
+ def make_contrib(): Unit = {
Isabelle_System.make_directory(Components.contrib(isabelle_dir))
File.write(Components.contrib(isabelle_dir, name = "README"),
"""This directory contains add-on components that contribute to the main
@@ -90,8 +86,8 @@
sealed case class Bundle_Info(
platform: Platform.Family.Value,
platform_description: String,
- name: String)
- {
+ name: String
+ ) {
def path: Path = Path.explode(name)
}
@@ -104,13 +100,10 @@
val ISABELLE_TAGS: Path = Path.explode("etc/ISABELLE_TAGS")
val ISABELLE_IDENTIFIER: Path = Path.explode("etc/ISABELLE_IDENTIFIER")
- object Release_Archive
- {
- def make(bytes: Bytes, rename: String = ""): Release_Archive =
- {
+ object Release_Archive {
+ def make(bytes: Bytes, rename: String = ""): Release_Archive = {
Isabelle_System.with_tmp_dir("tmp")(dir =>
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
- {
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => {
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
@@ -136,8 +129,11 @@
def read(path: Path, rename: String = ""): Release_Archive =
make(Bytes.read(path), rename = rename)
- def get(url: String, rename: String = "", progress: Progress = new Progress): Release_Archive =
- {
+ def get(
+ url: String,
+ rename: String = "",
+ progress: Progress = new Progress
+ ): Release_Archive = {
val bytes =
if (Path.is_wellformed(url)) Bytes.read(Path.explode(url))
else Isabelle_System.download(url, progress = progress).bytes
@@ -146,8 +142,7 @@
}
case class Release_Archive private[Build_Release](
- bytes: Bytes, id: String, tags: String, identifier: String)
- {
+ bytes: Bytes, id: String, tags: String, identifier: String) {
override def toString: String = identifier
}
@@ -157,8 +152,7 @@
/* bundled components */
- class Bundled(platform: Option[Platform.Family.Value] = None)
- {
+ class Bundled(platform: Option[Platform.Family.Value] = None) {
def detect(s: String): Boolean =
s.startsWith("#bundled") && !s.startsWith("#bundled ")
@@ -176,8 +170,7 @@
}
}
- def record_bundled_components(dir: Path): Unit =
- {
+ def record_bundled_components(dir: Path): Unit = {
val catalogs =
List("main", "bundled").map((_, new Bundled())) :::
Platform.Family.list.flatMap(platform =>
@@ -195,8 +188,7 @@
} yield bundled(line)).toList))
}
- def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) =
- {
+ def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = {
val Bundled = new Bundled(platform = Some(platform))
val components =
for { Bundled(name) <- Components.read_components(dir) } yield name
@@ -206,8 +198,7 @@
}
def activate_components(
- dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit =
- {
+ dir: Path, platform: Platform.Family.Value, more_names: List[String]): Unit = {
def contrib_name(name: String): String =
Components.contrib(name = name).implode
@@ -231,8 +222,8 @@
options: Options,
platform: Platform.Family.Value,
build_sessions: List[String],
- local_dir: Path): Unit =
- {
+ local_dir: Path
+ ): Unit = {
val server_option = "build_host_" + platform.toString
val ssh =
options.string(server_option) match {
@@ -244,11 +235,9 @@
case s => error("Malformed option " + server_option + ": " + quote(s))
}
try {
- Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar =>
- {
+ Isabelle_System.with_tmp_file("tmp", ext = "tar")(local_tmp_tar => {
execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .")
- ssh.with_tmp_dir(remote_dir =>
- {
+ ssh.with_tmp_dir(remote_dir => {
val remote_tmp_tar = remote_dir + Path.basic("tmp.tar")
ssh.write_file(remote_tmp_tar, local_tmp_tar)
val remote_commands =
@@ -269,8 +258,7 @@
/* Isabelle application */
- def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit =
- {
+ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n"): Unit = {
val title = "# Java runtime options"
File.write(path, (title :: options).map(_ + line_ending).mkString)
}
@@ -281,8 +269,7 @@
isabelle_name: String,
jdk_component: String,
classpath: List[Path],
- dock_icon: Boolean = false): Unit =
- {
+ dock_icon: Boolean = false): Unit = {
val script = """#!/usr/bin/env bash
#
# Author: Makarius
@@ -330,8 +317,7 @@
}
- def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit =
- {
+ def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String): Unit = {
File.write(path, """<?xml version="1.0" ?>
<!DOCTYPE plist PUBLIC "-//Apple//DTD PLIST 1.0//EN" "http://www.apple.com/DTDs/PropertyList-1.0.dtd">
<plist version="1.0">
@@ -394,8 +380,8 @@
def use_release_archive(
context: Release_Context,
archive: Release_Archive,
- id: String = ""): Unit =
- {
+ id: String = ""
+ ): Unit = {
if (id.nonEmpty && id != archive.id) {
error("Mismatch of release identification " + id + " vs. archive " + archive.id)
}
@@ -408,8 +394,8 @@
def build_release_archive(
context: Release_Context,
version: String,
- parallel_jobs: Int = 1): Unit =
- {
+ parallel_jobs: Int = 1
+ ): Unit = {
val progress = context.progress
val hg = Mercurial.repository(Path.ISABELLE_HOME)
@@ -497,8 +483,8 @@
website: Option[Path] = None,
build_sessions: List[String] = Nil,
build_library: Boolean = false,
- parallel_jobs: Int = 1): Unit =
- {
+ parallel_jobs: Int = 1
+ ): Unit = {
val progress = context.progress
@@ -510,8 +496,7 @@
Isabelle_System.rm_tree(context.dist_dir + path)
}
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path =>
- {
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz")(archive_path => {
Bytes.write(archive_path, archive.bytes)
val extract =
List("README", "NEWS", "ANNOUNCE", "COPYRIGHT", "CONTRIBUTORS", "doc").
@@ -533,8 +518,7 @@
progress.echo("\nApplication bundle for " + platform)
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
- {
+ Isabelle_System.with_tmp_dir("build_release")(tmp_dir => {
// release archive
execute_tar(tmp_dir, "-xzf " + File.bash_path(context.isabelle_archive))
@@ -578,13 +562,11 @@
if (opt.startsWith(s)) s + isabelle_name else opt
}) ::: List("-Disabelle.jedit_server=" + isabelle_name)
- val classpath: List[Path] =
- {
+ val classpath: List[Path] = {
val base = isabelle_target.absolute
val classpath1 = Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH"))
val classpath2 = Path.split(other_isabelle.getenv("ISABELLE_SETUP_CLASSPATH"))
- (classpath1 ::: classpath2).map(path =>
- {
+ (classpath1 ::: classpath2).map(path => {
val abs_path = path.absolute
File.relative_path(base, abs_path) match {
case Some(rel_path) => rel_path
@@ -833,8 +815,7 @@
progress.echo_warning("Library archive already exists: " + context.isabelle_library_archive)
}
else {
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
- {
+ Isabelle_System.with_tmp_dir("build_release")(tmp_dir => {
val bundle =
context.dist_dir + Path.explode(context.dist_name + "_" + Platform.family + ".tar.gz")
execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle))
@@ -862,8 +843,7 @@
/** command line entry point **/
- def main(args: Array[String]): Unit =
- {
+ def main(args: Array[String]): Unit = {
Command_Line.tool {
var afp_rev = ""
var components_base: Path = Components.default_components_base