--- a/src/Pure/Admin/build_release.scala Tue Apr 09 14:17:29 2019 +0200
+++ b/src/Pure/Admin/build_release.scala Tue Apr 09 15:09:09 2019 +0200
@@ -388,258 +388,254 @@
for (bundle_info <- bundle_infos) {
val bundle_archive = release.dist_dir + bundle_info.path
- if (bundle_archive.is_file && more_components.isEmpty)
- progress.echo_warning("Application bundle already exists: " + bundle_archive)
- else {
- val isabelle_name = release.dist_name
- val platform = bundle_info.platform
+ val isabelle_name = release.dist_name
+ val platform = bundle_info.platform
- progress.echo("\nApplication bundle for " + platform)
+ progress.echo("\nApplication bundle for " + platform)
- Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
- {
- // release archive
+ Isabelle_System.with_tmp_dir("build_release")(tmp_dir =>
+ {
+ // release archive
- execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
- val other_isabelle = release.other_isabelle(tmp_dir)
- val isabelle_target = other_isabelle.isabelle_home
+ execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive))
+ val other_isabelle = release.other_isabelle(tmp_dir)
+ val isabelle_target = other_isabelle.isabelle_home
- // bundled components
+ // bundled components
- progress.echo("Bundled components:")
+ progress.echo("Bundled components:")
- val contrib_dir = Components.contrib(isabelle_target)
+ val contrib_dir = Components.contrib(isabelle_target)
- val (bundled_components, jdk_component) =
- get_bundled_components(isabelle_target, platform)
+ val (bundled_components, jdk_component) =
+ get_bundled_components(isabelle_target, platform)
- Components.resolve(components_base, bundled_components,
- target_dir = Some(contrib_dir), progress = progress)
+ Components.resolve(components_base, bundled_components,
+ target_dir = Some(contrib_dir), progress = progress)
- val more_components_names =
- more_components.map(Components.unpack(contrib_dir, _, progress = progress))
+ val more_components_names =
+ more_components.map(Components.unpack(contrib_dir, _, progress = progress))
- Components.purge(contrib_dir, platform)
+ Components.purge(contrib_dir, platform)
- activate_components(isabelle_target, platform, more_components_names)
+ activate_components(isabelle_target, platform, more_components_names)
- // Java parameters
+ // Java parameters
- val java_options_title = "# Java runtime options"
- val java_options: List[String] =
- (for {
- variable <-
- List(
- "ISABELLE_JAVA_SYSTEM_OPTIONS",
- "JEDIT_JAVA_SYSTEM_OPTIONS",
- "JEDIT_JAVA_OPTIONS")
- opt <- Word.explode(other_isabelle.getenv(variable))
- } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
+ val java_options_title = "# Java runtime options"
+ val java_options: List[String] =
+ (for {
+ variable <-
+ List(
+ "ISABELLE_JAVA_SYSTEM_OPTIONS",
+ "JEDIT_JAVA_SYSTEM_OPTIONS",
+ "JEDIT_JAVA_OPTIONS")
+ opt <- Word.explode(other_isabelle.getenv(variable))
+ } yield opt) ::: List("-Disabelle.jedit_server=" + isabelle_name)
- val classpath: List[Path] =
+ val classpath: List[Path] =
+ {
+ val base = isabelle_target.absolute
+ Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
{
- val base = isabelle_target.absolute
- Path.split(other_isabelle.getenv("ISABELLE_CLASSPATH")).map(path =>
- {
- val abs_path = path.absolute
- File.relative_path(base, abs_path) match {
- case Some(rel_path) => rel_path
- case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
- }
- }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
- }
+ val abs_path = path.absolute
+ File.relative_path(base, abs_path) match {
+ case Some(rel_path) => rel_path
+ case None => error("Bad ISABELLE_CLASSPATH element: " + abs_path)
+ }
+ }) ::: List(Path.explode("src/Tools/jEdit/dist/jedit.jar"))
+ }
- val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
+ val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props")
- // application bundling
+ // application bundling
- platform match {
- case Platform.Family.linux =>
- File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
- terminate_lines(java_options_title :: java_options))
+ platform match {
+ case Platform.Family.linux =>
+ File.write(isabelle_target + Path.explode(isabelle_name + ".options"),
+ terminate_lines(java_options_title :: java_options))
- val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
- File.write(isabelle_run,
- File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
- .replaceAllLiterally("{CLASSPATH}",
- classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
- .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
- File.set_executable(isabelle_run, true)
+ val isabelle_run = isabelle_target + Path.explode(isabelle_name + ".run")
+ File.write(isabelle_run,
+ File.read(Path.explode("~~/Admin/Linux/Isabelle.run"))
+ .replaceAllLiterally("{CLASSPATH}",
+ classpath.map("$ISABELLE_HOME/" + _).mkString(":"))
+ .replaceAllLiterally("/jdk/", "/" + jdk_component + "/"))
+ File.set_executable(isabelle_run, true)
- val linux_app = isabelle_target + Path.explode("contrib/linux_app")
- File.move(linux_app + Path.explode("Isabelle"),
- isabelle_target + Path.explode(isabelle_name))
- Isabelle_System.rm_tree(linux_app)
+ val linux_app = isabelle_target + Path.explode("contrib/linux_app")
+ File.move(linux_app + Path.explode("Isabelle"),
+ isabelle_target + Path.explode(isabelle_name))
+ Isabelle_System.rm_tree(linux_app)
- val archive_name = isabelle_name + "_linux.tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- Bash.string(isabelle_name))
+ val archive_name = isabelle_name + "_linux.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ Bash.string(isabelle_name))
- case Platform.Family.macos =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
- .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
- .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
- .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
+ case Platform.Family.macos =>
+ File.write(isabelle_target + jedit_props,
+ File.read(isabelle_target + jedit_props)
+ .replaceAll("lookAndFeel=.*", "lookAndFeel=com.apple.laf.AquaLookAndFeel")
+ .replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d")
+ .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")
+ .replaceAll("plugin-blacklist.MacOSX.jar=true", "plugin-blacklist.MacOSX.jar="))
- // MacOS application bundle
+ // MacOS application bundle
- File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
+ File.move(isabelle_target + Path.explode("contrib/macos_app"), tmp_dir)
- val isabelle_app = Path.explode(isabelle_name + ".app")
- val app_dir = tmp_dir + isabelle_app
- File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
+ val isabelle_app = Path.explode(isabelle_name + ".app")
+ val app_dir = tmp_dir + isabelle_app
+ File.move(tmp_dir + Path.explode("macos_app/Isabelle.app"), app_dir)
- val app_contents = app_dir + Path.explode("Contents")
- val app_resources = app_contents + Path.explode("Resources")
- File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
+ val app_contents = app_dir + Path.explode("Contents")
+ val app_resources = app_contents + Path.explode("Resources")
+ File.move(tmp_dir + Path.explode(isabelle_name), app_resources)
- File.write(app_contents + Path.explode("Info.plist"),
- File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
- .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- .replaceAllLiterally("{JAVA_OPTIONS}",
- terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
+ File.write(app_contents + Path.explode("Info.plist"),
+ File.read(Path.explode("~~/Admin/MacOS/Info.plist"))
+ .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ .replaceAllLiterally("{JAVA_OPTIONS}",
+ terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
- for (cp <- classpath) {
- File.link(
- Path.explode("../Resources/" + isabelle_name + "/") + cp,
- app_contents + Path.explode("Java"),
- force = true)
- }
-
+ for (cp <- classpath) {
File.link(
- Path.explode("../Resources/" + isabelle_name + "/contrib/" +
- jdk_component + "/x86_64-darwin"),
- app_contents + Path.explode("PlugIns/bundled.jdk"),
+ Path.explode("../Resources/" + isabelle_name + "/") + cp,
+ app_contents + Path.explode("Java"),
force = true)
+ }
- File.link(
- Path.explode("../../Info.plist"),
- app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
- force = true)
+ File.link(
+ Path.explode("../Resources/" + isabelle_name + "/contrib/" +
+ jdk_component + "/x86_64-darwin"),
+ app_contents + Path.explode("PlugIns/bundled.jdk"),
+ force = true)
- File.link(
- Path.explode("Contents/Resources/" + isabelle_name),
- app_dir + Path.explode("Isabelle"),
- force = true)
+ File.link(
+ Path.explode("../../Info.plist"),
+ app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
+ force = true)
+
+ File.link(
+ Path.explode("Contents/Resources/" + isabelle_name),
+ app_dir + Path.explode("Isabelle"),
+ force = true)
- // application archive
+ // application archive
- val archive_name = isabelle_name + "_macos.tar.gz"
- progress.echo("Packaging " + archive_name + " ...")
- execute_tar(tmp_dir,
- "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
- File.bash_path(isabelle_app))
+ val archive_name = isabelle_name + "_macos.tar.gz"
+ progress.echo("Packaging " + archive_name + " ...")
+ execute_tar(tmp_dir,
+ "-czf " + File.bash_path(release.dist_dir + Path.explode(archive_name)) + " " +
+ File.bash_path(isabelle_app))
- case Platform.Family.windows =>
- File.write(isabelle_target + jedit_props,
- File.read(isabelle_target + jedit_props)
- .replaceAll("lookAndFeel=.*",
- "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
- .replaceAll("foldPainter=.*", "foldPainter=Square"))
+ case Platform.Family.windows =>
+ File.write(isabelle_target + jedit_props,
+ File.read(isabelle_target + jedit_props)
+ .replaceAll("lookAndFeel=.*",
+ "lookAndFeel=com.sun.java.swing.plaf.windows.WindowsLookAndFeel")
+ .replaceAll("foldPainter=.*", "foldPainter=Square"))
- // application launcher
+ // application launcher
- File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
+ File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir)
- val app_template = Path.explode("~~/Admin/Windows/launch4j")
+ val app_template = Path.explode("~~/Admin/Windows/launch4j")
- File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
- (java_options_title :: java_options).map(_ + "\r\n").mkString)
+ File.write(isabelle_target + Path.explode(isabelle_name + ".l4j.ini"),
+ (java_options_title :: java_options).map(_ + "\r\n").mkString)
- val isabelle_xml = Path.explode("isabelle.xml")
- val isabelle_exe = Path.explode(isabelle_name + ".exe")
+ val isabelle_xml = Path.explode("isabelle.xml")
+ val isabelle_exe = Path.explode(isabelle_name + ".exe")
- File.write(tmp_dir + isabelle_xml,
- File.read(app_template + isabelle_xml)
- .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- .replaceAllLiterally("{OUTFILE}",
- File.platform_path(isabelle_target + isabelle_exe))
- .replaceAllLiterally("{ICON}",
- File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
- .replaceAllLiterally("{SPLASH}",
- File.platform_path(app_template + Path.explode("isabelle.bmp")))
- .replaceAllLiterally("{CLASSPATH}",
- cat_lines(classpath.map(cp =>
- " <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
- .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
+ File.write(tmp_dir + isabelle_xml,
+ File.read(app_template + isabelle_xml)
+ .replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ .replaceAllLiterally("{OUTFILE}",
+ File.platform_path(isabelle_target + isabelle_exe))
+ .replaceAllLiterally("{ICON}",
+ File.platform_path(app_template + Path.explode("isabelle_transparent.ico")))
+ .replaceAllLiterally("{SPLASH}",
+ File.platform_path(app_template + Path.explode("isabelle.bmp")))
+ .replaceAllLiterally("{CLASSPATH}",
+ cat_lines(classpath.map(cp =>
+ " <cp>%EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + "</cp>")))
+ .replaceAllLiterally("\\jdk\\", "\\" + jdk_component + "\\"))
- execute(tmp_dir,
- "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+ execute(tmp_dir,
+ "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
- File.copy(app_template + Path.explode("manifest.xml"),
- isabelle_target + isabelle_exe.ext("manifest"))
+ File.copy(app_template + Path.explode("manifest.xml"),
+ isabelle_target + isabelle_exe.ext("manifest"))
- // Cygwin setup
+ // Cygwin setup
- val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
+ val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin")
- File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
+ File.copy(cygwin_template + Path.explode("Cygwin-Terminal.bat"), isabelle_target)
- val cygwin_mirror =
- File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
+ val cygwin_mirror =
+ File.read(isabelle_target + Path.explode("contrib/cygwin/isabelle/cygwin_mirror"))
- val cygwin_bat = Path.explode("Cygwin-Setup.bat")
- File.write(isabelle_target + cygwin_bat,
- File.read(cygwin_template + cygwin_bat)
- .replaceAllLiterally("{MIRROR}", cygwin_mirror))
- File.set_executable(isabelle_target + cygwin_bat, true)
+ val cygwin_bat = Path.explode("Cygwin-Setup.bat")
+ File.write(isabelle_target + cygwin_bat,
+ File.read(cygwin_template + cygwin_bat)
+ .replaceAllLiterally("{MIRROR}", cygwin_mirror))
+ File.set_executable(isabelle_target + cygwin_bat, true)
- for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
- val path = Path.explode(name)
- File.copy(cygwin_template + path,
- isabelle_target + Path.explode("contrib/cygwin") + path)
- }
+ for (name <- List("isabelle/postinstall", "isabelle/rebaseall")) {
+ val path = Path.explode(name)
+ File.copy(cygwin_template + path,
+ isabelle_target + Path.explode("contrib/cygwin") + path)
+ }
- execute(isabelle_target,
- """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
- (if (Platform.is_macos) "-perm +100" else "-executable") +
- " -print0 > contrib/cygwin/isabelle/executables")
+ execute(isabelle_target,
+ """find . -type f -not -name "*.exe" -not -name "*.dll" """ +
+ (if (Platform.is_macos) "-perm +100" else "-executable") +
+ " -print0 > contrib/cygwin/isabelle/executables")
- execute(isabelle_target,
- """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
- """> contrib/cygwin/isabelle/symlinks""")
+ execute(isabelle_target,
+ """find . -type l -exec echo "{}" ";" -exec readlink "{}" ";" """ +
+ """> contrib/cygwin/isabelle/symlinks""")
- execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
+ execute(isabelle_target, """find . -type l -exec rm "{}" ";" """)
- File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
+ File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "")
- // executable archive (self-extracting 7z)
+ // executable archive (self-extracting 7z)
- val archive_name = isabelle_name + ".7z"
- val exe_archive = tmp_dir + Path.explode(archive_name)
- exe_archive.file.delete
+ val archive_name = isabelle_name + ".7z"
+ val exe_archive = tmp_dir + Path.explode(archive_name)
+ exe_archive.file.delete
- progress.echo("Packaging " + archive_name + " ...")
- execute(tmp_dir,
- "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
- if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
+ progress.echo("Packaging " + archive_name + " ...")
+ execute(tmp_dir,
+ "7z -y -bd a " + File.bash_path(exe_archive) + " " + Bash.string(isabelle_name))
+ if (!exe_archive.is_file) error("Failed to create archive: " + exe_archive)
- val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
- val sfx_txt =
- File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
- replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
+ val sfx_exe = tmp_dir + Path.explode("windows_app/7zsd_All_x64.sfx")
+ val sfx_txt =
+ File.read(Path.explode("~~/Admin/Windows/Installer/sfx.txt")).
+ replaceAllLiterally("{ISABELLE_NAME}", isabelle_name)
- Bytes.write(release.dist_dir + isabelle_exe,
- Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
- File.set_executable(release.dist_dir + isabelle_exe, true)
- }
- })
- progress.echo("DONE")
- }
+ Bytes.write(release.dist_dir + isabelle_exe,
+ Bytes.read(sfx_exe) + Bytes(sfx_txt) + Bytes.read(exe_archive))
+ File.set_executable(release.dist_dir + isabelle_exe, true)
+ }
+ })
+ progress.echo("DONE")
}