diff --git a/lib/scripts/java-gui-setup b/lib/scripts/java-gui-setup new file mode 100755 --- /dev/null +++ b/lib/scripts/java-gui-setup @@ -0,0 +1,11 @@ +#!/usr/bin/env bash +# +# java-gui-setup --- platform-specific setup for Java/Swing GUI applications + +if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ] +then + JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" + JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" + defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || + defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null +fi diff --git a/src/Pure/Admin/build_release.scala b/src/Pure/Admin/build_release.scala --- a/src/Pure/Admin/build_release.scala +++ b/src/Pure/Admin/build_release.scala @@ -1,938 +1,933 @@ /* Title: Pure/Admin/build_release.scala Author: Makarius Build full Isabelle distribution from repository. */ package isabelle object Build_Release { /** release info **/ sealed case class Bundle_Info( platform: Platform.Family.Value, platform_description: String, name: String) { def path: Path = Path.explode(name) } class Release private[Build_Release]( progress: Progress, val date: Date, val dist_name: String, val dist_dir: Path, val dist_version: String, val ident: String) { val isabelle_dir: Path = dist_dir + Path.explode(dist_name) val isabelle_archive: Path = dist_dir + Path.explode(dist_name + ".tar.gz") val isabelle_library_archive: Path = dist_dir + Path.explode(dist_name + "_library.tar.gz") def other_isabelle(dir: Path): Other_Isabelle = Other_Isabelle(dir + Path.explode(dist_name), isabelle_identifier = dist_name + "-build", progress = progress) def bundle_info(platform: Platform.Family.Value): Bundle_Info = platform match { case Platform.Family.linux => Bundle_Info(platform, "Linux", dist_name + "_linux.tar.gz") case Platform.Family.macos => Bundle_Info(platform, "macOS", dist_name + "_macos.tar.gz") case Platform.Family.windows => Bundle_Info(platform, "Windows", dist_name + ".exe") } } /** generated content **/ /* patch release */ private val getsettings_path = Path.explode("lib/scripts/getsettings") private val ISABELLE_ID = """ISABELLE_ID="(.+)"""".r def patch_release(release: Release, is_official: Boolean) { val dir = release.isabelle_dir for (name <- List("src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala")) { File.change(dir + Path.explode(name), _.replace("val is_identified = false", "val is_identified = true") .replace("val is_official = false", "val is_official = " + is_official)) } File.change(dir + getsettings_path, _.replace("ISABELLE_ID=\"\"", "ISABELLE_ID=" + quote(release.ident)) .replace("ISABELLE_IDENTIFIER=\"\"", "ISABELLE_IDENTIFIER=" + quote(release.dist_name))) File.change(dir + Path.explode("lib/html/library_index_header.template"), _.replace("{ISABELLE}", release.dist_name)) for { name <- List( "src/Pure/System/distribution.ML", "src/Pure/System/distribution.scala", "lib/Tools/version") } { File.change(dir + Path.explode(name), _.replace("repository version", release.dist_version)) } File.change(dir + Path.explode("README"), _.replace("some repository version of Isabelle", release.dist_version)) } /* ANNOUNCE */ def make_announce(release: Release) { File.write(release.isabelle_dir + Path.explode("ANNOUNCE"), """ IMPORTANT NOTE ============== This is a snapshot of Isabelle/""" + release.ident + """ from the repository. """) } /* NEWS */ def make_news(other_isabelle: Other_Isabelle, dist_version: String) { val target = other_isabelle.isabelle_home + Path.explode("doc") val target_fonts = Isabelle_System.make_directory(target + Path.explode("fonts")) other_isabelle.copy_fonts(target_fonts) HTML.write_document(target, "NEWS.html", List(HTML.title("NEWS (" + dist_version + ")")), List( HTML.chapter("NEWS"), HTML.source( Symbol.decode(File.read(other_isabelle.isabelle_home + Path.explode("NEWS")))))) } /* bundled components */ class Bundled(platform: Option[Platform.Family.Value] = None) { def detect(s: String): Boolean = s.startsWith("#bundled") && !s.startsWith("#bundled ") def apply(name: String): String = "#bundled" + (platform match { case None => "" case Some(plat) => "-" + plat }) + ":" + name private val Pattern1 = ("""^#bundled:(.*)$""").r private val Pattern2 = ("""^#bundled-(.*):(.*)$""").r def unapply(s: String): Option[String] = s match { case Pattern1(name) => Some(name) case Pattern2(Platform.Family(plat), name) if platform == Some(plat) => Some(name) case _ => None } } def record_bundled_components(dir: Path) { val catalogs = List("main", "bundled").map((_, new Bundled())) ::: default_platform_families.flatMap(platform => List(platform.toString, "bundled-" + platform.toString). map((_, new Bundled(platform = Some(platform))))) File.append(Components.components(dir), terminate_lines("#bundled components" :: (for { (catalog, bundled) <- catalogs.iterator path = Components.admin(dir) + Path.basic(catalog) if path.is_file line <- split_lines(File.read(path)) if line.nonEmpty && !line.startsWith("#") && !line.startsWith("jedit_build") } yield bundled(line)).toList)) } 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) if !name.startsWith("jedit_build") } yield name val jdk_component = components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component") (components, jdk_component) } def activate_components(dir: Path, platform: Platform.Family.Value, more_names: List[String]) { def contrib_name(name: String): String = Components.contrib(name = name).implode val Bundled = new Bundled(platform = Some(platform)) Components.write_components(dir, Components.read_components(dir).flatMap(line => line match { case Bundled(name) => if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name)) else None case _ => if (Bundled.detect(line)) None else Some(line) }) ::: more_names.map(contrib_name)) } def make_contrib(dir: Path) { Isabelle_System.make_directory(Components.contrib(dir)) File.write(Components.contrib(dir, "README"), """This directory contains add-on components that contribute to the main Isabelle distribution. Separate licensing conditions apply, see each directory individually. """) } /** build release **/ private def execute(dir: Path, script: String): Unit = Isabelle_System.bash(script, cwd = dir.file).check private def execute_tar(dir: Path, args: String): Unit = Isabelle_System.gnutar(args, dir = dir).check /* build heaps on remote server */ private def remote_build_heaps( options: Options, platform: Platform.Family.Value, build_sessions: List[String], local_dir: Path) { val server_option = "build_host_" + platform.toString options.string(server_option) match { case SSH.Target(user, host) => using(SSH.open_session(options, host = host, user = user))(ssh => { Isabelle_System.with_tmp_file("tmp", "tar")(local_tmp_tar => { execute_tar(local_dir, "-cf " + File.bash_path(local_tmp_tar) + " .") 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 = List( "cd " + File.bash_path(remote_dir), "tar -xf tmp.tar", "./bin/isabelle build -o system_heaps -b -- " + Bash.strings(build_sessions), "tar -cf tmp.tar heaps") ssh.execute(remote_commands.mkString(" && ")).check ssh.read_file(remote_tmp_tar, local_tmp_tar) }) execute_tar(local_dir, "-xf " + File.bash_path(local_tmp_tar)) }) }) case s => error("Bad " + server_option + ": " + quote(s)) } } /* Isabelle application */ def make_isabelle_options(path: Path, options: List[String], line_ending: String = "\n") { val title = "# Java runtime options" File.write(path, (title :: options).map(_ + line_ending).mkString) } def make_isabelle_app( path: Path, isabelle_home_prefix: String, jdk_component: String, classpath: List[Path], dock_icon: Boolean = false) { val script = """#!/usr/bin/env bash # # Author: Makarius # # Main Isabelle application script. # minimal Isabelle environment ISABELLE_HOME="$(cd "$(dirname "$0")"; cd "$(pwd -P)/""" + isabelle_home_prefix + """"; pwd)" source "$ISABELLE_HOME/lib/scripts/isabelle-platform" #paranoia settings -- avoid intrusion of alien options unset "_JAVA_OPTIONS" unset "JAVA_TOOL_OPTIONS" #paranoia settings -- avoid problems of Java/Swing versus XIM/IBus etc. unset XMODIFIERS COMPONENT="$ISABELLE_HOME/contrib/""" + jdk_component + """" source "$COMPONENT/etc/settings" # main declare -a JAVA_OPTIONS=($(perl -p -e 's,#.*$,,g;' "$ISABELLE_HOME/Isabelle.options")) -if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then - JAVA_VERSION="$("$ISABELLE_JDK_HOME/bin/java" -version 2>&1 | head -n 1 | cut -d '"' -f2)" - JAVA_DOMAIN="com.azul.zulu.${JAVA_VERSION}.java" - defaults read "$JAVA_DOMAIN" AppleWindowTabbingMode >/dev/null 2>/dev/null || - defaults write "$JAVA_DOMAIN" AppleWindowTabbingMode manual >/dev/null 2>/dev/null -fi +"$ISABELLE_HOME/lib/scripts/java-gui-setup" exec "$ISABELLE_JDK_HOME/bin/java" \ "-Disabelle.root=$ISABELLE_HOME" "${JAVA_OPTIONS[@]}" \ -classpath """" + classpath.map(p => "$ISABELLE_HOME/" + p.implode).mkString(":") + """" \ "-splash:$ISABELLE_HOME/lib/logo/isabelle.gif" \ """ + (if (dock_icon) """"-Xdock:icon=$ISABELLE_HOME/lib/logo/isabelle_transparent-128.png" \ """ else "") + """isabelle.Main "$@" """ File.write(path, script) File.set_executable(path, true) } def make_isabelle_plist(path: Path, isabelle_name: String, isabelle_rev: String) { File.write(path, """ CFBundleDevelopmentRegion English CFBundleIconFile isabelle.icns CFBundleIdentifier de.tum.in.isabelle CFBundleDisplayName """ + isabelle_name + """ CFBundleInfoDictionaryVersion 6.0 CFBundleName """ + isabelle_name + """ CFBundlePackageType APPL CFBundleShortVersionString """ + isabelle_name + """ CFBundleSignature ???? CFBundleVersion """ + isabelle_rev + """ NSHumanReadableCopyright LSMinimumSystemVersion 10.11 LSApplicationCategoryType public.app-category.developer-tools NSHighResolutionCapable true NSSupportsAutomaticGraphicsSwitching true CFBundleDocumentTypes CFBundleTypeExtensions thy CFBundleTypeIconFile theory.icns CFBundleTypeName Isabelle theory file CFBundleTypeRole Editor LSTypeIsPackage """) } /* main */ private val default_platform_families: List[Platform.Family.Value] = List(Platform.Family.linux, Platform.Family.windows, Platform.Family.macos) def build_release(base_dir: Path, options: Options, components_base: Path = Components.default_components_base, progress: Progress = new Progress, rev: String = "", afp_rev: String = "", official_release: Boolean = false, proper_release_name: Option[String] = None, platform_families: List[Platform.Family.Value] = default_platform_families, more_components: List[Path] = Nil, website: Option[Path] = None, build_sessions: List[String] = Nil, build_library: Boolean = false, parallel_jobs: Int = 1): Release = { val hg = Mercurial.repository(Path.explode("$ISABELLE_HOME")) val release = { val date = Date.now() val dist_name = proper_release_name getOrElse ("Isabelle_" + Date.Format.date(date)) val dist_dir = (base_dir + Path.explode("dist-" + dist_name)).absolute val version = proper_string(rev) orElse proper_release_name getOrElse "tip" val ident = try { hg.id(version) } catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) } val dist_version = proper_release_name match { case Some(name) => name + ": " + Date.Format("LLLL uuuu")(date) case None => "Isabelle repository snapshot " + ident + " " + Date.Format.date(date) } new Release(progress, date, dist_name, dist_dir, dist_version, ident) } /* make distribution */ if (release.isabelle_archive.is_file) { progress.echo_warning("Release archive already exists: " + release.isabelle_archive) val archive_ident = Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val getsettings = Path.explode(release.dist_name) + getsettings_path execute_tar(tmp_dir, "-xzf " + File.bash_path(release.isabelle_archive) + " " + File.bash_path(getsettings)) split_lines(File.read(tmp_dir + getsettings)) .collectFirst({ case ISABELLE_ID(ident) => ident }) .getOrElse(error("Failed to read ISABELLE_ID from " + release.isabelle_archive)) }) if (release.ident != archive_ident) { error("Mismatch of release identification " + release.ident + " vs. archive " + archive_ident) } } else { progress.echo_warning("Producing release archive " + release.isabelle_archive + " ...") Isabelle_System.make_directory(release.dist_dir) if (release.isabelle_dir.is_dir) error("Directory " + release.isabelle_dir + " already exists") progress.echo_warning("Retrieving Mercurial repository version " + release.ident) hg.archive(release.isabelle_dir.expand.implode, rev = release.ident, options = "--type files") for (name <- List(".hg_archival.txt", ".hgtags", ".hgignore", "README_REPOSITORY")) { (release.isabelle_dir + Path.explode(name)).file.delete } progress.echo_warning("Preparing distribution " + quote(release.dist_name)) patch_release(release, proper_release_name.isDefined && official_release) if (proper_release_name.isEmpty) make_announce(release) make_contrib(release.isabelle_dir) execute(release.isabelle_dir, """find . -print | xargs chmod -f u+rw""") record_bundled_components(release.isabelle_dir) /* build tools and documentation */ val other_isabelle = release.other_isabelle(release.dist_dir) other_isabelle.init_settings( other_isabelle.init_components(components_base = components_base, catalogs = List("main"))) other_isabelle.resolve_components(echo = true) try { val export_classpath = "export CLASSPATH=" + Bash.string(other_isabelle.getenv("ISABELLE_CLASSPATH")) + "\n" other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) } try { other_isabelle.bash( "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check } catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) } make_news(other_isabelle, release.dist_version) for (name <- List("Admin", "browser_info", "heaps")) { Isabelle_System.rm_tree(other_isabelle.isabelle_home + Path.explode(name)) } other_isabelle.cleanup() progress.echo_warning("Creating distribution archive " + release.isabelle_archive) def execute_dist_name(script: String): Unit = Isabelle_System.bash(script, cwd = release.dist_dir.file, env = Isabelle_System.settings() + ("DIST_NAME" -> release.dist_name)).check execute_dist_name(""" set -e chmod -R a+r "$DIST_NAME" chmod -R u+w "$DIST_NAME" chmod -R g=o "$DIST_NAME" find "$DIST_NAME" -type f "(" -name "*.thy" -o -name "*.ML" -o -name "*.scala" ")" -print | xargs chmod -f u-w """) execute_tar(release.dist_dir, "-czf " + File.bash_path(release.isabelle_archive) + " " + Bash.string(release.dist_name)) execute_dist_name(""" set -e mv "$DIST_NAME" "${DIST_NAME}-old" mkdir "$DIST_NAME" mv "${DIST_NAME}-old/README" "${DIST_NAME}-old/NEWS" "${DIST_NAME}-old/ANNOUNCE" \ "${DIST_NAME}-old/COPYRIGHT" "${DIST_NAME}-old/CONTRIBUTORS" "$DIST_NAME" mkdir "$DIST_NAME/doc" mv "${DIST_NAME}-old/doc/"*.pdf \ "${DIST_NAME}-old/doc/"*.html \ "${DIST_NAME}-old/doc/"*.css \ "${DIST_NAME}-old/doc/fonts" \ "${DIST_NAME}-old/doc/Contents" "$DIST_NAME/doc" rm -f Isabelle && ln -sf "$DIST_NAME" Isabelle rm -rf "${DIST_NAME}-old" """) } /* make application bundles */ val bundle_infos = platform_families.map(release.bundle_info) for (bundle_info <- bundle_infos) { val isabelle_name = release.dist_name val platform = bundle_info.platform progress.echo("\nApplication bundle for " + platform) 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 // bundled components progress.echo("Bundled components:") val contrib_dir = Components.contrib(isabelle_target) val (bundled_components, jdk_component) = get_bundled_components(isabelle_target, platform) Components.resolve(components_base, bundled_components, target_dir = Some(contrib_dir), copy_dir = Some(release.dist_dir + Path.explode("contrib")), progress = progress) val more_components_names = more_components.map(Components.unpack(contrib_dir, _, progress = progress)) Components.purge(contrib_dir, platform) activate_components(isabelle_target, platform, more_components_names) // Java parameters 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 { val s = "-Dapple.awt.application.name=" if (opt.startsWith(s)) s + isabelle_name else opt }) ::: List("-Disabelle.jedit_server=" + isabelle_name) val classpath: List[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 jedit_options = Path.explode("src/Tools/jEdit/etc/options") val jedit_props = Path.explode("src/Tools/jEdit/dist/properties/jEdit.props") // build heaps if (build_sessions.nonEmpty) { progress.echo("Building heaps ...") remote_build_heaps(options, platform, build_sessions, isabelle_target) } // application bundling platform match { case Platform.Family.linux => File.change(isabelle_target + jedit_options, _.replaceAll("jedit_reset_font_size : int =.*", "jedit_reset_font_size : int = 24")) File.change(isabelle_target + jedit_props, _.replaceAll("console.fontsize=.*", "console.fontsize=18") .replaceAll("helpviewer.fontsize=.*", "helpviewer.fontsize=18") .replaceAll("metal.primary.fontsize=.*", "metal.primary.fontsize=18") .replaceAll("metal.secondary.fontsize=.*", "metal.secondary.fontsize=18") .replaceAll("view.fontsize=.*", "view.fontsize=24") .replaceAll("view.gutter.fontsize=.*", "view.gutter.fontsize=16")) make_isabelle_options( isabelle_target + Path.explode("Isabelle.options"), java_options) make_isabelle_app( isabelle_target + Path.explode("lib/scripts/Isabelle_app"), "../..", jdk_component, classpath) 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)) case Platform.Family.macos => File.change(isabelle_target + jedit_props, _.replaceAll("delete-line.shortcut=.*", "delete-line.shortcut=C+d") .replaceAll("delete.shortcut2=.*", "delete.shortcut2=A+d")) // MacOS application bundle val isabelle_app = Path.explode(isabelle_name + ".app") val app_dir = tmp_dir + isabelle_app val app_contents = app_dir + Path.explode("Contents") val app_resources = Isabelle_System.make_directory(app_contents + Path.explode("Resources")) File.move(tmp_dir + Path.explode(isabelle_name), app_resources) val isabelle_home = Path.explode("Contents/Resources/" + isabelle_name) val isabelle_options = Path.explode("Isabelle.options") File.link( isabelle_home, app_dir + Path.explode("Isabelle"), force = true) File.link( isabelle_home + isabelle_options, app_dir + isabelle_options, force = true) for (icon <- List("lib/logo/isabelle.icns", "lib/logo/theory.icns")) { File.copy(app_dir + isabelle_home + Path.explode(icon), app_resources) } make_isabelle_app( app_dir + Path.explode(isabelle_name), isabelle_home.implode, jdk_component, classpath, dock_icon = true) make_isabelle_options( app_dir + isabelle_options, java_options ::: List("-Disabelle.app=true")) make_isabelle_plist( app_contents + Path.explode("Info.plist"), isabelle_name, release.ident) // 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)) case Platform.Family.windows => File.change(isabelle_target + jedit_props, _.replaceAll("foldPainter=.*", "foldPainter=Square")) // application launcher File.move(isabelle_target + Path.explode("contrib/windows_app"), tmp_dir) val app_template = Path.explode("~~/Admin/Windows/launch4j") make_isabelle_options( isabelle_target + Path.explode(isabelle_name + ".l4j.ini"), java_options, line_ending = "\r\n") 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) .replace("{ISABELLE_NAME}", isabelle_name) .replace("{OUTFILE}", File.platform_path(isabelle_target + isabelle_exe)) .replace("{ICON}", File.platform_path(app_template + Path.explode("isabelle_transparent.ico"))) .replace("{SPLASH}", File.platform_path(app_template + Path.explode("isabelle.bmp"))) .replace("{CLASSPATH}", cat_lines(classpath.map(cp => " %EXEDIR%\\" + File.platform_path(cp).replace('/', '\\') + ""))) .replace("\\jdk\\", "\\" + jdk_component + "\\")) 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")) // Cygwin setup val cygwin_template = Path.explode("~~/Admin/Windows/Cygwin") 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_bat = Path.explode("Cygwin-Setup.bat") File.write(isabelle_target + cygwin_bat, File.read(cygwin_template + cygwin_bat).replace("{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) } 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 rm "{}" ";" """) File.write(isabelle_target + Path.explode("contrib/cygwin/isabelle/uninitialized"), "") // executable archive (self-extracting 7z) 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) 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")) .replace("{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") } /* minimal website */ for (dir <- website) { val website_platform_bundles = for { bundle_info <- bundle_infos if (release.dist_dir + bundle_info.path).is_file } yield (bundle_info.name, bundle_info) val isabelle_link = HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident, HTML.text("Isabelle/" + release.ident)) val afp_link = HTML.link(AFP.repos_source + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev)) HTML.write_document(dir, "index.html", List(HTML.title(release.dist_name)), List( HTML.section(release.dist_name), HTML.subsection("Platforms"), HTML.itemize( website_platform_bundles.map({ case (bundle, bundle_info) => List(HTML.link(bundle, HTML.text(bundle_info.platform_description))) })), HTML.subsection("Repositories"), HTML.itemize( 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) } /* HTML library */ if (build_library) { if (release.isabelle_library_archive.is_file) { progress.echo_warning("Library archive already exists: " + release.isabelle_library_archive) } else { Isabelle_System.with_tmp_dir("build_release")(tmp_dir => { val bundle = release.dist_dir + Path.explode(release.dist_name + "_" + Platform.family + ".tar.gz") execute_tar(tmp_dir, "-xzf " + File.bash_path(bundle)) val other_isabelle = release.other_isabelle(tmp_dir) Isabelle_System.make_directory(other_isabelle.etc) File.write(other_isabelle.etc_preferences, "ML_system_64 = true\n") other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs + " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" + " -o system_heaps -c -a -d '~~/src/Benchmarks'", echo = true).check other_isabelle.isabelle_home_user.file.delete execute(tmp_dir, "chmod -R a+r " + Bash.string(release.dist_name)) execute(tmp_dir, "chmod -R g=o " + Bash.string(release.dist_name)) execute_tar(tmp_dir, "-czf " + File.bash_path(release.isabelle_library_archive) + " " + Bash.string(release.dist_name + "/browser_info")) }) } } release } /** command line entry point **/ def main(args: Array[String]) { Command_Line.tool { var afp_rev = "" var components_base: Path = Components.default_components_base var official_release = false var proper_release_name: Option[String] = None var website: Option[Path] = None var build_sessions: List[String] = Nil var more_components: List[Path] = Nil var parallel_jobs = 1 var build_library = false var options = Options.init() var platform_families = default_platform_families var rev = "" val getopts = Getopts(""" Usage: Admin/build_release [OPTIONS] BASE_DIR Options are: -A REV corresponding AFP changeset id -C DIR base directory for Isabelle components (default: """ + Components.default_components_base + """) -O official release (not release-candidate) -R RELEASE proper release with name -W WEBSITE produce minimal website in given directory -b SESSIONS build platform-specific session images (separated by commas) -c ARCHIVE clean bundling with additional component .tar.gz archive -j INT maximum number of parallel jobs (default 1) -l build library -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) -p NAMES platform families (default: """ + default_platform_families.mkString(",") + """) -r REV Mercurial changeset id (default: RELEASE or tip) Build Isabelle release in base directory, using the local repository clone. """, "A:" -> (arg => afp_rev = arg), "C:" -> (arg => components_base = Path.explode(arg)), "O" -> (_ => official_release = true), "R:" -> (arg => proper_release_name = Some(arg)), "W:" -> (arg => website = Some(Path.explode(arg))), "b:" -> (arg => build_sessions = space_explode(',', arg)), "c:" -> (arg => { val path = Path.explode(arg) Components.Archive.get_name(path.file_name) more_components = more_components ::: List(path) }), "j:" -> (arg => parallel_jobs = Value.Int.parse(arg)), "l" -> (_ => build_library = true), "o:" -> (arg => options = options + arg), "p:" -> (arg => platform_families = space_explode(',', arg).map(Platform.Family.parse)), "r:" -> (arg => rev = arg)) val more_args = getopts(args) val base_dir = more_args match { case List(base_dir) => base_dir case _ => getopts.usage() } val progress = new Console_Progress() if (platform_families.contains(Platform.Family.windows) && !Isabelle_System.bash("7z i").ok) error("Building for windows requires 7z") build_release(Path.explode(base_dir), options, components_base = components_base, progress = progress, rev = rev, afp_rev = afp_rev, official_release = official_release, proper_release_name = proper_release_name, website = website, platform_families = if (platform_families.isEmpty) default_platform_families else platform_families, more_components = more_components, build_sessions = build_sessions, build_library = build_library, parallel_jobs = parallel_jobs) } } } diff --git a/src/Tools/jEdit/lib/Tools/jedit b/src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit +++ b/src/Tools/jEdit/lib/Tools/jedit @@ -1,417 +1,419 @@ #!/usr/bin/env bash # # Author: Makarius # # DESCRIPTION: Isabelle/jEdit interface wrapper ## sources declare -a SOURCES0=( "src/Tools/jEdit/src-base/dockable.scala" "src/Tools/jEdit/src-base/isabelle_encoding.scala" "src/Tools/jEdit/src-base/jedit_lib.scala" "src/Tools/jEdit/src-base/pide_docking_framework.scala" "src/Tools/jEdit/src-base/plugin.scala" "src/Tools/jEdit/src-base/syntax_style.scala" ) declare -a RESOURCES0=( "src/Tools/jEdit/src-base/Isabelle_Base.props" "src/Tools/jEdit/src-base/services.xml" ) declare -a SOURCES=( "src/Tools/jEdit/src/active.scala" "src/Tools/jEdit/src/completion_popup.scala" "src/Tools/jEdit/src/context_menu.scala" "src/Tools/jEdit/src/debugger_dockable.scala" "src/Tools/jEdit/src/document_model.scala" "src/Tools/jEdit/src/document_view.scala" "src/Tools/jEdit/src/documentation_dockable.scala" "src/Tools/jEdit/src/fold_handling.scala" "src/Tools/jEdit/src/font_info.scala" "src/Tools/jEdit/src/graphview_dockable.scala" "src/Tools/jEdit/src/info_dockable.scala" "src/Tools/jEdit/src/isabelle.scala" "src/Tools/jEdit/src/isabelle_encoding.scala" "src/Tools/jEdit/src/isabelle_export.scala" "src/Tools/jEdit/src/isabelle_options.scala" "src/Tools/jEdit/src/isabelle_session.scala" "src/Tools/jEdit/src/isabelle_sidekick.scala" "src/Tools/jEdit/src/isabelle_vfs.scala" "src/Tools/jEdit/src/jedit_bibtex.scala" "src/Tools/jEdit/src/jedit_editor.scala" "src/Tools/jEdit/src/jedit_lib.scala" "src/Tools/jEdit/src/jedit_options.scala" "src/Tools/jEdit/src/jedit_rendering.scala" "src/Tools/jEdit/src/jedit_resources.scala" "src/Tools/jEdit/src/jedit_sessions.scala" "src/Tools/jEdit/src/jedit_spell_checker.scala" "src/Tools/jEdit/src/keymap_merge.scala" "src/Tools/jEdit/src/monitor_dockable.scala" "src/Tools/jEdit/src/output_dockable.scala" "src/Tools/jEdit/src/plugin.scala" "src/Tools/jEdit/src/pretty_text_area.scala" "src/Tools/jEdit/src/pretty_tooltip.scala" "src/Tools/jEdit/src/process_indicator.scala" "src/Tools/jEdit/src/protocol_dockable.scala" "src/Tools/jEdit/src/query_dockable.scala" "src/Tools/jEdit/src/raw_output_dockable.scala" "src/Tools/jEdit/src/rich_text_area.scala" "src/Tools/jEdit/src/scala_console.scala" "src/Tools/jEdit/src/session_build.scala" "src/Tools/jEdit/src/simplifier_trace_dockable.scala" "src/Tools/jEdit/src/simplifier_trace_window.scala" "src/Tools/jEdit/src/sledgehammer_dockable.scala" "src/Tools/jEdit/src/state_dockable.scala" "src/Tools/jEdit/src/status_widget.scala" "src/Tools/jEdit/src/symbols_dockable.scala" "src/Tools/jEdit/src/syntax_style.scala" "src/Tools/jEdit/src/syslog_dockable.scala" "src/Tools/jEdit/src/text_overview.scala" "src/Tools/jEdit/src/text_structure.scala" "src/Tools/jEdit/src/theories_dockable.scala" "src/Tools/jEdit/src/timing_dockable.scala" "src/Tools/jEdit/src/token_markup.scala" ) declare -a RESOURCES=( "src/Tools/jEdit/src/actions.xml" "src/Tools/jEdit/src/dockables.xml" "src/Tools/jEdit/src/Isabelle.props" "src/Tools/jEdit/src/jEdit.props" "src/Tools/jEdit/src/services.xml" "src/Tools/jEdit/src/modes/isabelle-ml.xml" "src/Tools/jEdit/src/modes/isabelle-news.xml" "src/Tools/jEdit/src/modes/isabelle-options.xml" "src/Tools/jEdit/src/modes/isabelle-root.xml" "src/Tools/jEdit/src/modes/isabelle.xml" "src/Tools/jEdit/src/modes/sml.xml" ) ## diagnostics PRG="$(basename "$0")" function usage() { echo echo "Usage: isabelle $PRG [OPTIONS] [FILES ...]" echo echo " Options are:" echo " -A NAME ancestor session for option -R (default: parent)" echo " -D NAME=X set JVM system property" echo " -J OPTION add JVM runtime option" echo " (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" echo " -R NAME build image with requirements from other sessions" echo " -b build only" echo " -d DIR include session directory" echo " -f fresh build" echo " -i NAME include session in name-space of theories" echo " -j OPTION add jEdit runtime option" echo " (default $JEDIT_OPTIONS)" echo " -l NAME logic session name" echo " -m MODE add print mode for output" echo " -n no build of session image on startup" echo " -p CMD ML process command prefix (process policy)" echo " -s system build mode for session image (system_heaps=true)" echo " -u user build mode for session image (system_heaps=false)" echo echo " Start jEdit with Isabelle plugin setup and open FILES" echo " (default \"$USER_HOME/Scratch.thy\" or \":\" for empty buffer)." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } function failed() { fail "Failed!" } ## process command line # options BUILD_ONLY=false FRESH_BUILD="" ML_PROCESS_POLICY="" JEDIT_LOGIC_ANCESTOR="" JEDIT_LOGIC_REQUIREMENTS="" JEDIT_INCLUDE_SESSIONS="" JEDIT_SESSION_DIRS="-" JEDIT_LOGIC="" JEDIT_PRINT_MODE="" JEDIT_NO_BUILD="" JEDIT_BUILD_MODE="default" function getoptions() { OPTIND=1 while getopts "A:BFD:J:R:bd:fi:j:l:m:np:su" OPT do case "$OPT" in A) JEDIT_LOGIC_ANCESTOR="$OPTARG" ;; D) JAVA_ARGS["${#JAVA_ARGS[@]}"]="-D$OPTARG" ;; J) JAVA_ARGS["${#JAVA_ARGS[@]}"]="$OPTARG" ;; R) JEDIT_LOGIC="$OPTARG" JEDIT_LOGIC_REQUIREMENTS="true" ;; b) BUILD_ONLY=true ;; d) JEDIT_SESSION_DIRS="$JEDIT_SESSION_DIRS:$OPTARG" ;; i) if [ -z "$JEDIT_INCLUDE_SESSIONS" ]; then JEDIT_INCLUDE_SESSIONS="$OPTARG" else JEDIT_INCLUDE_SESSIONS="$JEDIT_INCLUDE_SESSIONS:$OPTARG" fi ;; f) FRESH_BUILD="true" ;; j) ARGS["${#ARGS[@]}"]="$OPTARG" ;; l) JEDIT_LOGIC="$OPTARG" ;; m) if [ -z "$JEDIT_PRINT_MODE" ]; then JEDIT_PRINT_MODE="$OPTARG" else JEDIT_PRINT_MODE="$JEDIT_PRINT_MODE,$OPTARG" fi ;; n) JEDIT_NO_BUILD="true" ;; p) ML_PROCESS_POLICY="$OPTARG" ;; s) JEDIT_BUILD_MODE="system" ;; u) JEDIT_BUILD_MODE="user" ;; \?) usage ;; esac done } eval "declare -a JAVA_ARGS=($JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)" declare -a ARGS=() declare -a OPTIONS; eval "OPTIONS=($ISABELLE_JEDIT_OPTIONS)" getoptions "${OPTIONS[@]}" getoptions "$@" shift $(($OPTIND - 1)) # args while [ "$#" -gt 0 ]; do ARGS["${#ARGS[@]}"]="$(platform_path "$1")" shift done ## dependencies if [ -e "$ISABELLE_HOME/Admin/build" ]; then isabelle browser -b || exit $? if [ -n "$FRESH_BUILD" ]; then "$ISABELLE_HOME/Admin/build" jars_fresh || exit $? else "$ISABELLE_HOME/Admin/build" jars || exit $? fi elif [ -n "$FRESH_BUILD" ]; then echo >&2 "### Ignoring fresh build option: not a repository clone" FRESH_BUILD="" fi JEDIT_BUILD_JAR="$ISABELLE_JEDIT_BUILD_VERSION/jedit.jar" declare -a JEDIT_BUILD_JARS=( "Code2HTML.jar" "CommonControls.jar" "Console.jar" "ErrorList.jar" "Highlight.jar" "kappalayout.jar" "Navigator.jar" "SideKick.jar" "idea-icons.jar" "jsr305-2.0.0.jar" ) # target pushd "$ISABELLE_HOME" >/dev/null || failed TARGET_DIR="src/Tools/jEdit/dist" TARGET_JAR0="$TARGET_DIR/jars/Isabelle-jEdit-base.jar" TARGET_JAR="$TARGET_DIR/jars/Isabelle-jEdit.jar" TARGET_SHASUM="$TARGET_DIR/Isabelle-jEdit.shasum" declare -a TARGET_DEPS=("lib/classes/Pure.jar" "$TARGET_DIR/jedit.jar") for DEP in "${JEDIT_BUILD_JARS[@]}" do TARGET_DEPS["${#TARGET_DEPS[@]}"]="$TARGET_DIR/jars/$DEP" done function target_shasum() ( shasum -a1 -b "$TARGET_JAR0" "$TARGET_JAR" "${TARGET_DEPS[@]}" \ "${SOURCES0[@]}" "${RESOURCES0[@]}" "${SOURCES[@]}" "${RESOURCES[@]}" 2>/dev/null ) function target_clean() { rm -rf "$ISABELLE_HOME/$TARGET_DIR" } [ -n "$FRESH_BUILD" ] && target_clean ## build BUILD_DIR="$TARGET_DIR/build" function init_resources () { mkdir -p "$BUILD_DIR" || failed cp -p -R "$@" "$BUILD_DIR/." } function compile_sources() { ( #FIXME workarounds for scalac 2.11.0 export CYGWIN="nodosfilewarning" function stty() { :; } export -f stty for DEP in "${TARGET_DEPS[@]}" do classpath "$DEP" done export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")" isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d "$BUILD_DIR" "$@" ) || fail "Failed to compile sources" } function make_jar() { isabelle_jdk jar -c -f "$1" -C "$BUILD_DIR" . || failed rm -rf "$ISABELLE_HOME/$BUILD_DIR" } target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null if [ -e "$ISABELLE_HOME/Admin/build" -a "$?" -ne 0 ]; then echo "### Building Isabelle/jEdit ..." [ -z "$ISABELLE_JEDIT_BUILD_HOME" ] && \ fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component" target_clean || failed mkdir -p "$TARGET_DIR" || failed cp -p -R "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." "$TARGET_DIR/." for DEP in "${JEDIT_BUILD_JARS[@]}" do cp -p "$ISABELLE_JEDIT_BUILD_HOME/contrib/$DEP" "$TARGET_DIR/jars/." done init_resources "${RESOURCES0[@]}" compile_sources "${SOURCES0[@]}" make_jar "$TARGET_JAR0" classpath "$TARGET_JAR0" init_resources "${RESOURCES[@]}" cp src/Tools/jEdit/src/jEdit.props "$TARGET_DIR/properties/." cp -p -R -f "src/Tools/jEdit/src/modes/." "$TARGET_DIR/modes/." perl -i -e 'while (<>) { if (m/FILE="ml.xml"/ or m/FILE_NAME_GLOB="...sml,ml."/ or m/FILE_NAME_GLOB="..ftl"/) { } elsif (m/NAME="javacc"/) { print qq!\n\n!; print qq!\n\n!; print qq!\n\n!; print qq!\n\n!; print qq!\n\n!; print; } elsif (m/NAME="sqr"/) { print qq!\n\n!; print; } else { print; } }' "$TARGET_DIR/modes/catalog" ( cd "$TARGET_DIR" isabelle_jdk jar -x -f jedit.jar cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \ "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" \ "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed isabelle_jdk jar -c -f jedit.jar -e org.gjt.sp.jedit.jEdit org || failed rm -rf META-INF org ) compile_sources "${SOURCES[@]}" make_jar "$TARGET_JAR" target_shasum > "$TARGET_SHASUM" cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.6.0manual-a4.pdf" "$TARGET_DIR/doc/jedit-manual.pdf" cp "$TARGET_DIR/doc/CHANGES.txt" "$TARGET_DIR/doc/jedit-changes" cat > "$TARGET_DIR/doc/Contents" </dev/null if [ "$BUILD_ONLY" = false ] then + "$ISABELLE_HOME/lib/scripts/java-gui-setup" + export JEDIT_SESSION_DIRS JEDIT_LOGIC JEDIT_LOGIC_ANCESTOR JEDIT_LOGIC_REQUIREMENTS \ JEDIT_INCLUDE_SESSIONS JEDIT_PRINT_MODE JEDIT_NO_BUILD JEDIT_BUILD_MODE export JEDIT_ML_PROCESS_POLICY="$ML_PROCESS_POLICY" classpath "$JEDIT_HOME/dist/jedit.jar" exec isabelle java -splash:"$(platform_path "$ISABELLE_HOME/lib/logo/isabelle.gif")" \ "${JAVA_ARGS[@]}" isabelle.Main "${ARGS[@]}" fi