diff --git a/src/Pure/Admin/build_easychair.scala b/src/Pure/Admin/build_easychair.scala --- a/src/Pure/Admin/build_easychair.scala +++ b/src/Pure/Admin/build_easychair.scala @@ -1,102 +1,99 @@ /* Title: Pure/Admin/build_easychair.scala Author: Makarius Build Isabelle component for Easychair LaTeX style. See also https://easychair.org/publications/for_authors */ package isabelle object Build_Easychair { /* build easychair component */ val default_url = "https://easychair.org/publications/easychair.zip" def build_easychair( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { - Isabelle_System.require_command("unzip", test = "-h") - Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(download_file), - cwd = download_dir.file).check + Isabelle_System.extract(download_file, download_dir) val easychair_dir = File.get_dir(download_dir, title = download_url) /* component */ val version = Library.try_unprefix("EasyChair", easychair_dir.file_name) .getOrElse("Failed to detect version from " + quote(easychair_dir.file_name)) val component = "easychair-" + 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(easychair_dir, component_dir.path) Isabelle_System.make_directory(component_dir.etc) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_EASYCHAIR_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is the Easychair style for authors from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_easychair", "build component for Easychair LaTeX style", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_easychair [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for Easychair LaTeX style. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_easychair(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_eptcs.scala b/src/Pure/Admin/build_eptcs.scala --- a/src/Pure/Admin/build_eptcs.scala +++ b/src/Pure/Admin/build_eptcs.scala @@ -1,100 +1,96 @@ /* Title: Pure/Admin/build_eptcs.scala Author: Makarius Build Isabelle component for EPTCS LaTeX style. See also: - http://style.eptcs.org - https://github.com/EPTCS/style/releases */ package isabelle object Build_EPTCS { /* build eptcs component */ val default_url = "https://github.com/EPTCS/style/releases/download" val default_version = "1.7.0" def build_eptcs( base_url: String = default_url, version: String = default_version, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { - Isabelle_System.require_command("unzip", test = "-h") - - /* component */ val component = "eptcs-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* download */ val download_url = base_url + "/v" + version + "/eptcsstyle.zip" Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.download_file(download_url, download_file, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(download_file), - cwd = component_dir.path.file).check + Isabelle_System.extract(download_file, component_dir.path) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_EPTCS_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is the EPTCS style from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_eptcs", "build component for EPTCS LaTeX style", Scala_Project.here, { args => var target_dir = Path.current var base_url = default_url var version = default_version val getopts = Getopts(""" Usage: isabelle build_eptcs [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") -V VERSION version (default: """" + default_version + """") Build component for EPTCS LaTeX style. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), "V:" -> (arg => version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_eptcs(base_url = base_url, version = version, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_foiltex.scala b/src/Pure/Admin/build_foiltex.scala --- a/src/Pure/Admin/build_foiltex.scala +++ b/src/Pure/Admin/build_foiltex.scala @@ -1,111 +1,108 @@ /* Title: Pure/Admin/build_foiltex.scala Author: Makarius Build Isabelle component for FoilTeX. See also https://ctan.org/pkg/foiltex */ package isabelle object Build_Foiltex { /* build FoilTeX component */ val default_url = "https://mirrors.ctan.org/macros/latex/contrib/foiltex.zip" def build_foiltex( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { - Isabelle_System.require_command("unzip", test = "-h") - Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(download_file), - cwd = download_dir.file).check + Isabelle_System.extract(download_file, download_dir) 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 version = { val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r split_lines(File.read(foiltex_dir + README_flt)) .collectFirst({ case Version(v) => v }) .getOrElse(error("Failed to detect version in " + README_flt)) } 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) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_FOILTEX_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is FoilTeX from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_foiltex", "build component for FoilTeX", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_foiltex [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for FoilTeX: slides in LaTeX. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_foiltex(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_jdk.scala b/src/Pure/Admin/build_jdk.scala --- a/src/Pure/Admin/build_jdk.scala +++ b/src/Pure/Admin/build_jdk.scala @@ -1,229 +1,223 @@ /* Title: Pure/Admin/build_jdk.scala Author: Makarius Build Isabelle jdk component from original platform installations. */ package isabelle import java.io.{File => JFile} import java.nio.file.Files import java.nio.file.attribute.PosixFilePermission import scala.util.matching.Regex object Build_JDK { /* platform and version information */ sealed case class JDK_Platform( platform_name: String, platform_regex: Regex, exe: String = "java", macos_home: Boolean = false, jdk_version: String = "" ) { override def toString: String = platform_name def platform_path: Path = Path.explode(platform_name) def detect(jdk_dir: Path): Option[JDK_Platform] = { val major_version = { val Major_Version = """.*jdk(\d+).*$""".r val jdk_name = jdk_dir.file.getName jdk_name match { case Major_Version(s) => s case _ => error("Cannot determine major version from " + quote(jdk_name)) } } val path = jdk_dir + Path.explode("bin") + Path.explode(exe) if (path.is_file) { val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out if (platform_regex.matches(file_descr)) { val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r val version_lines = Isabelle_System.bash("strings " + File.bash_path(path)).check .out_lines.flatMap({ case Version(s) => Some(s) case _ => None }) version_lines match { case List(jdk_version) => Some(copy(jdk_version = jdk_version)) case _ => error("Expected unique version within executable " + path) } } else None } else None } } val templates: List[JDK_Platform] = List( JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true), JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r), JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true), JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r), JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe")) /* README */ def readme(jdk_version: String): String = """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also https://www.azul.com/downloads/zulu-community/?package=jdk The main license is GPL2, but some modules are covered by other (more liberal) licenses, see legal/* for details. Linux, Windows, macOS all work uniformly, depending on platform-specific subdirectories. """ /* settings */ val settings: String = """# -*- shell-script -*- :mode=shellscript: case "$ISABELLE_PLATFORM_FAMILY" in linux) ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; windows) ISABELLE_JAVA_PLATFORM="$ISABELLE_WINDOWS_PLATFORM64" ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; macos) if [ -n "$ISABELLE_APPLE_PLATFORM64" -a -d "$COMPONENT/$ISABELLE_APPLE_PLATFORM64" ] then ISABELLE_JAVA_PLATFORM="$ISABELLE_APPLE_PLATFORM64" else ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64" fi ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM" ;; esac """ /* extract archive */ def extract_archive(dir: Path, archive: Path): JDK_Platform = { try { val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp")) - if (archive.get_ext == "zip") { - Isabelle_System.bash( - "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check - } - else { - Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check - } + Isabelle_System.extract(archive, tmp_dir) val jdk_dir = File.get_dir(tmp_dir, title = archive.file_name) val platform = templates.view.flatMap(_.detect(jdk_dir)) .headOption.getOrElse(error("Failed to detect JDK platform")) val platform_dir = dir + platform.platform_path if (platform_dir.is_dir) error("Directory already exists: " + platform_dir) Isabelle_System.move_file(jdk_dir, platform_dir) platform } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) } } /* build jdk */ def build_jdk( archives: List[Path], progress: Progress = new Progress, target_dir: Path = Path.current ): Unit = { if (Platform.is_windows) error("Cannot build jdk on Windows") Isabelle_System.with_tmp_dir("jdk") { dir => progress.echo("Extracting ...") val platforms = archives.map(extract_archive(dir, _)) val jdk_version = platforms.map(_.jdk_version).distinct match { case List(version) => version case Nil => error("No archives") case versions => error("Archives contain multiple JDK versions: " + commas_quote(versions)) } templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name)) match { case Nil => case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name))) } val jdk_name = "jdk-" + jdk_version val jdk_path = Path.explode(jdk_name) val component_dir = Components.Directory.create(dir + jdk_path, progress = progress) File.write(component_dir.settings, settings) File.write(component_dir.README, readme(jdk_version)) for (platform <- platforms) { Isabelle_System.move_file(dir + platform.platform_path, component_dir.path) } for (file <- File.find_files(component_dir.path.file, include_dirs = true)) { val path = file.toPath val perms = Files.getPosixFilePermissions(path) perms.add(PosixFilePermission.OWNER_READ) perms.add(PosixFilePermission.GROUP_READ) perms.add(PosixFilePermission.OTHERS_READ) perms.add(PosixFilePermission.OWNER_WRITE) if (file.isDirectory) { perms.add(PosixFilePermission.OWNER_WRITE) perms.add(PosixFilePermission.OWNER_EXECUTE) perms.add(PosixFilePermission.GROUP_EXECUTE) perms.add(PosixFilePermission.OTHERS_EXECUTE) } Files.setPosixFilePermissions(path, perms) } progress.echo("Archiving ...") Isabelle_System.gnutar( "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives", Scala_Project.here, { args => var target_dir = Path.current val getopts = Getopts(""" Usage: isabelle build_jdk [OPTIONS] ARCHIVES... Options are: -D DIR target directory (default ".") Build jdk component from tar.gz archives, with original jdk archives for Linux, Windows, and macOS. """, "D:" -> (arg => target_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.isEmpty) getopts.usage() val archives = more_args.map(Path.explode) val progress = new Console_Progress() build_jdk(archives = archives, progress = progress, target_dir = target_dir) }) } diff --git a/src/Pure/Admin/build_jedit.scala b/src/Pure/Admin/build_jedit.scala --- a/src/Pure/Admin/build_jedit.scala +++ b/src/Pure/Admin/build_jedit.scala @@ -1,544 +1,543 @@ /* Title: Pure/Admin/build_jedit.scala Author: Makarius Build component for jEdit text-editor. */ package isabelle import java.nio.charset.Charset import scala.jdk.CollectionConverters._ object Build_JEdit { /* modes */ object Mode { val empty: Mode = new Mode("", "", Nil) val init: Mode = empty + ("noWordSep" -> """_'?⇩\^<>""") + ("unalignedOpenBrackets" -> "{[(«‹⟨⌈⌊⦇⟦⦃⦉") + ("unalignedCloseBrackets" -> "⦊⦄⟧⦈⌋⌉⟩›»)]}") + ("tabSize" -> "2") + ("indentSize" -> "2") val list: List[Mode] = { val isabelle_news: Mode = init.define("isabelle-news", "Isabelle NEWS") val isabelle: Mode = init.define("isabelle", "Isabelle theory") + ("commentStart" -> "(*") + ("commentEnd" -> "*)") val isabelle_ml: Mode = isabelle.define("isabelle-ml", "Isabelle/ML") val isabelle_root: Mode = isabelle.define("isabelle-root", "Isabelle session root") val isabelle_options: Mode = isabelle.define("isabelle-options", "Isabelle options") val sml: Mode = init.define("sml", "Standard ML") + ("commentStart" -> "(*") + ("commentEnd" -> "*)") + ("noWordSep" -> "_'") List(isabelle_news, isabelle, isabelle_ml, isabelle_root, isabelle_options, sml) } } final case class Mode private(name: String, description: String, rev_props: Properties.T) { override def toString: String = name def define(a: String, b: String): Mode = new Mode(a, b, rev_props) def + (entry: Properties.Entry): Mode = new Mode(name, description, Properties.put(rev_props, entry)) def write(dir: Path): Unit = { require(name.nonEmpty && description.nonEmpty, "Bad Isabelle/jEdit mode content") val properties = rev_props.reverse.map(p => Symbol.spaces(4) + XML.string_of_tree(XML.elem(Markup("PROPERTY", List("NAME" -> p._1, "VALUE" -> p._2))))) File.write(dir + Path.basic(name).xml, """ """ + properties.mkString("\n", "\n", "") + """ """) } } /* build jEdit component */ private val download_jars: List[(String, String)] = List( "https://repo1.maven.org/maven2/com/google/code/findbugs/jsr305/3.0.2/jsr305-3.0.2.jar" -> "jsr305-3.0.2.jar") private val download_plugins: List[(String, String)] = List( "Code2HTML" -> "0.7", "CommonControls" -> "1.7.4", "Console" -> "5.1.4", "ErrorList" -> "2.4.0", "Highlight" -> "2.5", "Navigator" -> "2.7", "SideKick" -> "1.8") private def exclude_package(name: String): Boolean = name.startsWith("de.masters_of_disaster.ant") || name == "doclet" || name == "installer" def build_jedit( component_path: Path, version: String, original: Boolean = false, java_home: Path = default_java_home, progress: Progress = new Progress ): Unit = { Isabelle_System.require_command("ant", test = "-version") Isabelle_System.require_command("patch") - Isabelle_System.require_command("unzip", test = "-h") val component_dir = Components.Directory.create(component_path, progress = progress) /* jEdit directory */ val jedit = "jedit" + version val jedit_patched = jedit + "-patched" val jedit_dir = Isabelle_System.make_directory(component_path + Path.basic(jedit)) val jedit_patched_dir = component_path + Path.basic(jedit_patched) def download_jedit(dir: Path, name: String, target_name: String = ""): Path = { val jedit_name = jedit + name val url = "https://sourceforge.net/projects/jedit/files/jedit/" + version + "/" + jedit_name + "/download" val path = dir + Path.basic(proper_string(target_name) getOrElse jedit_name) Isabelle_System.download_file(url, path, progress = progress) path } Isabelle_System.with_tmp_dir("build") { tmp_dir => /* original version */ val install_path = download_jedit(tmp_dir, "install.jar") Isabelle_System.bash("""export CLASSPATH="" isabelle_java java -Duser.home=""" + File.bash_platform_path(tmp_dir) + " -jar " + File.bash_platform_path(install_path) + " auto " + File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check val source_path = download_jedit(tmp_dir, "source.tar.bz2") Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check /* patched version */ Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir) val source_dir = jedit_patched_dir + Path.basic("jEdit") val org_source_dir = source_dir + Path.basic("org") val tmp_source_dir = tmp_dir + Path.basic("jEdit") progress.echo("Patching jEdit sources ...") for { file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).sortBy(_.getName) name = file.getName if !File.is_backup(name) } { progress.bash("patch -p2 < " + File.bash_path(File.path(file)), cwd = source_dir.file, echo = true).check } for { theme <- List("classic", "tango") } { val path = Path.explode("org/gjt/sp/jedit/icons/themes/" + theme + "/32x32/apps/isabelle.gif") Isabelle_System.copy_file(Path.explode("~~/lib/logo/isabelle_transparent-32.gif"), source_dir + path) } progress.echo("Building jEdit ...") Isabelle_System.copy_dir(source_dir, tmp_source_dir) progress.bash("env JAVA_HOME=" + File.bash_platform_path(java_home) + " ant", cwd = tmp_source_dir.file, echo = true).check Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir) val java_sources = (for { file <- File.find_files(org_source_dir.file, file => File.is_java(file.getName)) package_name <- Scala_Project.package_name(File.path(file)) if !exclude_package(package_name) } yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode).sorted File.write(component_dir.build_props, "module = " + jedit_patched + "/jedit.jar\n" + "no_build = true\n" + "requirements = env:JEDIT_JARS\n" + ("sources =" :: java_sources.sorted.map(" " + _)).mkString("", " \\\n", "\n")) } /* jars */ val jars_dir = Isabelle_System.make_directory(jedit_patched_dir + Path.basic("jars")) for { (url, name) <- download_jars } { Isabelle_System.download_file(url, jars_dir + Path.basic(name), progress = progress) } for { (name, vers) <- download_plugins } { Isabelle_System.with_tmp_file("tmp", ext = "zip") { zip_path => val url = "https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" + name + "-" + vers + "-bin.zip/download" Isabelle_System.download_file(url, zip_path, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check + Isabelle_System.extract(zip_path, jars_dir) } } /* resources */ val keep_encodings = List("ISO-8859-1", "ISO-8859-15", "US-ASCII", "UTF-8", "windows-1252") val drop_encodings = Charset.availableCharsets().keySet().asScala.toList.sorted.filterNot(keep_encodings.contains) File.write(jedit_patched_dir + Path.explode("properties/jEdit.props"), """#jEdit properties autoReloadDialog=false buffer.deepIndent=false buffer.encoding=UTF-8-Isabelle buffer.indentSize=2 buffer.lineSeparator=\n buffer.maxLineLen=100 buffer.noTabs=true buffer.sidekick.keystroke-parse=false buffer.tabSize=2 buffer.undoCount=1000 close-docking-area.shortcut2=C+e C+CIRCUMFLEX complete-word.shortcut= console.dock-position=floating console.encoding=UTF-8 console.font=Isabelle DejaVu Sans Mono console.fontsize=14 delete-line.shortcut=A+d delete.shortcut2=C+d """ + drop_encodings.map(a => "encoding.opt-out." + a + "=true").mkString("\n") + """ encodingDetectors=BOM XML-PI buffer-local-property end.shortcut= expand-abbrev.shortcut2=CA+SPACE expand-folds.shortcut= fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII firstTime=false focus-buffer-switcher.shortcut2=A+CIRCUMFLEX foldPainter=Circle gatchan.highlight.overview=false helpviewer.font=Isabelle DejaVu Serif helpviewer.fontsize=12 home.shortcut= hypersearch-results.dock-position=right insert-newline-indent.shortcut= insert-newline.shortcut= isabelle-debugger.dock-position=floating isabelle-documentation.dock-position=left isabelle-export-browser.label=Browse theory exports isabelle-output.dock-position=bottom isabelle-output.height=174 isabelle-output.width=412 isabelle-query.dock-position=bottom isabelle-session-browser.label=Browse session information isabelle-simplifier-trace.dock-position=floating isabelle-sledgehammer.dock-position=bottom isabelle-state.dock-position=right isabelle-symbols.dock-position=bottom isabelle-theories.dock-position=right isabelle.antiquoted_cartouche.label=Make antiquoted cartouche isabelle.complete-word.label=Complete word isabelle.complete.label=Complete Isabelle text isabelle.complete.shortcut2=C+b isabelle.control-bold.label=Control bold isabelle.control-bold.shortcut=C+e RIGHT isabelle.control-emph.label=Control emphasized isabelle.control-emph.shortcut=C+e LEFT isabelle.control-reset.label=Control reset isabelle.control-reset.shortcut=C+e BACK_SPACE isabelle.control-sub.label=Control subscript isabelle.control-sub.shortcut=C+e DOWN isabelle.control-sup.label=Control superscript isabelle.control-sup.shortcut=C+e UP isabelle.decrease-font-size.label=Decrease font size isabelle.decrease-font-size.shortcut2=C+SUBTRACT isabelle.decrease-font-size.shortcut=C+MINUS isabelle.decrease-font-size2.label=Decrease font size (clone) isabelle.draft.label=Show draft in browser isabelle.exclude-word-permanently.label=Exclude word permanently isabelle.exclude-word.label=Exclude word isabelle.first-error.label=Go to first error isabelle.first-error.shortcut=CS+a isabelle.goto-entity.label=Go to definition of formal entity at caret isabelle.goto-entity.shortcut=CS+d isabelle.include-word-permanently.label=Include word permanently isabelle.include-word.label=Include word isabelle.increase-font-size.label=Increase font size isabelle.increase-font-size.shortcut2=C+ADD isabelle.increase-font-size.shortcut=C+PLUS isabelle.increase-font-size2.label=Increase font size (clone) isabelle.increase-font-size2.shortcut=C+EQUALS isabelle.java-monitor.label=Java/VM monitor isabelle.last-error.label=Go to last error isabelle.last-error.shortcut=CS+z isabelle.message.label=Show message isabelle.message.shortcut=CS+m isabelle.newline.label=Newline with indentation of Isabelle keywords isabelle.newline.shortcut=ENTER isabelle.next-error.label=Go to next error isabelle.next-error.shortcut=CS+n isabelle.options.label=Isabelle options isabelle.prev-error.label=Go to previous error isabelle.prev-error.shortcut=CS+p isabelle.preview.label=Show preview in browser isabelle.reset-continuous-checking.label=Reset continuous checking isabelle.reset-font-size.label=Reset font size isabelle.reset-node-required.label=Reset node required isabelle.reset-words.label=Reset non-permanent words isabelle.select-entity.label=Select all occurences of formal entity at caret isabelle.select-entity.shortcut=CS+ENTER isabelle.set-continuous-checking.label=Set continuous checking isabelle.set-node-required.label=Set node required isabelle.toggle-breakpoint.label=Toggle Breakpoint isabelle.toggle-continuous-checking.label=Toggle continuous checking isabelle.toggle-continuous-checking.shortcut=C+e ENTER isabelle.toggle-node-required.label=Toggle node required isabelle.toggle-node-required.shortcut=C+e SPACE isabelle.tooltip.label=Show tooltip isabelle.tooltip.shortcut=CS+b isabelle.update-state.label=Update state output isabelle.update-state.shortcut=S+ENTER lang.usedefaultlocale=false largefilemode=full line-end.shortcut=END line-home.shortcut=HOME logo.icon.medium=32x32/apps/isabelle.gif lookAndFeel=com.formdev.flatlaf.FlatLightLaf match-bracket.shortcut2=C+9 metal.primary.font=Isabelle DejaVu Sans metal.primary.fontsize=12 metal.secondary.font=Isabelle DejaVu Sans metal.secondary.fontsize=12 navigator.showOnToolbar=true new-file-in-mode.shortcut= next-bracket.shortcut2=C+e C+9 options.shortcuts.deletekeymap.label=Delete options.shortcuts.duplicatekeymap.dialog.title=Keymap name options.shortcuts.duplicatekeymap.label=Duplicate options.shortcuts.resetkeymap.dialog.title=Reset keymap options.shortcuts.resetkeymap.label=Reset options.textarea.lineSpacing=1 plugin-blacklist.MacOSX.jar=true plugin.MacOSXPlugin.altDispatcher=false plugin.MacOSXPlugin.disableOption=true prev-bracket.shortcut2=C+e C+8 print.font=Isabelle DejaVu Sans Mono print.glyphVector=true recent-buffer.shortcut2=C+CIRCUMFLEX restore.remote=false restore=false search.subdirs.toggle=true select-block.shortcut2=C+8 sidekick-tree.dock-position=right sidekick.auto-complete-popup-get-focus=true sidekick.buffer-save-parse=true sidekick.complete-delay=0 sidekick.complete-instant.toggle=false sidekick.complete-popup.accept-characters=\\t sidekick.complete-popup.insert-characters= sidekick.persistentFilter=true sidekick.showFilter=true sidekick.splitter.location=721 systrayicon=false tip.show=false toggle-full-screen.shortcut2=S+F11 toggle-multi-select.shortcut2=C+NUMBER_SIGN toggle-rect-select.shortcut2=A+NUMBER_SIGN twoStageSave=false vfs.browser.dock-position=left vfs.favorite.0.type=1 vfs.favorite.0=$ISABELLE_HOME vfs.favorite.1.type=1 vfs.favorite.1=$ISABELLE_HOME_USER vfs.favorite.2.type=1 vfs.favorite.2=$JEDIT_HOME vfs.favorite.3.type=1 vfs.favorite.3=$JEDIT_SETTINGS vfs.favorite.4.type=1 vfs.favorite.4=isabelle-export: vfs.favorite.5.type=1 vfs.favorite.5=isabelle-session: view.antiAlias=subpixel HRGB view.blockCaret=true view.caretBlink=false view.docking.framework=PIDE view.eolMarkers=false view.extendedState=0 view.font=Isabelle DejaVu Sans Mono view.fontsize=18 view.fracFontMetrics=false view.gutter.font=Isabelle DejaVu Sans Mono view.gutter.fontsize=12 view.gutter.lineNumbers=false view.gutter.selectionAreaWidth=18 view.height=850 view.middleMousePaste=true view.showToolbar=true view.status.memory.background=#666699 view.status=( mode , fold , encoding ) locked wrap multiSelect rectSelect overwrite lineSep buffersets task-monitor java-status ml-status errors clock view.thickCaret=true view.width=1200 xml-insert-closing-tag.shortcut= """) val modes_dir = jedit_patched_dir + Path.basic("modes") Mode.list.foreach(_.write(modes_dir)) File.change_lines(modes_dir + Path.basic("catalog")) { _.flatMap(line => if (line.containsSlice("FILE=\"ml.xml\"") || line.containsSlice("FILE_NAME_GLOB=\"*.{sml,ml}\"") || line.containsSlice("FILE_NAME_GLOB=\"*.ftl\"")) Nil else if (line.containsSlice("NAME=\"jamon\"")) { List( """""", "", """""", "", """""", "", """""", "", """""", "", line) } else if (line.containsSlice("NAME=\"sqr\"")) { List( """""", "", line) } else List(line)) } /* doc */ val doc_dir = jedit_patched_dir + Path.basic("doc") download_jedit(doc_dir, "manual-a4.pdf", target_name = "jedit-manual.pdf") Isabelle_System.copy_file( doc_dir + Path.basic("CHANGES.txt"), doc_dir + Path.basic("jedit-changes")) File.write(doc_dir + Path.basic("Contents"), """Original jEdit Documentation jedit-manual jEdit User's Guide jedit-changes jEdit Version History """) /* make patch */ File.write(component_path + Path.basic(jedit).patch, Isabelle_System.make_patch(component_path, Path.basic(jedit), Path.basic(jedit_patched))) if (!original) Isabelle_System.rm_tree(jedit_dir) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: JEDIT_HOME="$COMPONENT/""" + jedit_patched + """" JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """ JEDIT_JAR="$JEDIT_HOME/jedit.jar" classpath "$JEDIT_JAR" JEDIT_SETTINGS="$ISABELLE_HOME_USER/jedit" JEDIT_OPTIONS="-reuseview -nobackground -nosplash -log=9" JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4g -Xss16m" JEDIT_JAVA_SYSTEM_OPTIONS="-Duser.language=en -Dawt.useSystemAAFontSettings=on -Dswing.aatext=true -Dapple.laf.useScreenMenuBar=true -Dapple.awt.application.name=Isabelle" ISABELLE_DOCS="$ISABELLE_DOCS:$JEDIT_HOME/doc" """) /* README */ File.write(component_dir.README, """This is a slightly patched version of jEdit """ + version + """ from https://sourceforge.net/projects/jedit/files/jedit with some additional plugins jars from https://sourceforge.net/projects/jedit-plugins/files Makarius """ + Date.Format.date(Date.now()) + "\n") } /** Isabelle tool wrappers **/ val default_version = "5.6.0" def default_java_home: Path = Path.explode("$JAVA_HOME").expand val isabelle_tool = Isabelle_Tool("build_jedit", "build Isabelle component from the jEdit text-editor", Scala_Project.here, { args => var target_dir = Path.current var java_home = default_java_home var original = false var version = default_version val getopts = Getopts(""" Usage: isabelle build_jedit [OPTIONS] Options are: -D DIR target directory (default ".") -J JAVA_HOME Java version for building jedit.jar (e.g. version 11) -O retain copy of original jEdit directory -V VERSION jEdit version (default: """ + quote(default_version) + """) Build auxiliary jEdit component from original sources, with some patches. """, "D:" -> (arg => target_dir = Path.explode(arg)), "J:" -> (arg => java_home = Path.explode(arg)), "O" -> (_ => original = true), "V:" -> (arg => version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val component_dir = target_dir + Path.basic("jedit-" + Date.Format.alt_date(Date.now())) val progress = new Console_Progress() build_jedit(component_dir, version, original = original, java_home = java_home, progress = progress) }) } diff --git a/src/Pure/Admin/build_llncs.scala b/src/Pure/Admin/build_llncs.scala --- a/src/Pure/Admin/build_llncs.scala +++ b/src/Pure/Admin/build_llncs.scala @@ -1,111 +1,108 @@ /* Title: Pure/Admin/build_llncs.scala Author: Makarius Build Isabelle component for Springer LaTeX LNCS style. See also: - https://ctan.org/pkg/llncs?lang=en - https://www.springer.com/gp/computer-science/lncs/conference-proceedings-guidelines */ package isabelle object Build_LLNCS { /* build llncs component */ val default_url = "https://mirrors.ctan.org/macros/latex/contrib/llncs.zip" def build_llncs( download_url: String = default_url, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { - Isabelle_System.require_command("unzip", test = "-h") - Isabelle_System.with_tmp_file("download", ext = "zip") { download_file => Isabelle_System.with_tmp_dir("download") { download_dir => /* download */ Isabelle_System.download_file(download_url, download_file, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(download_file), - cwd = download_dir.file).check + Isabelle_System.extract(download_file, download_dir) 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 version = { val Version = """^_.* v(.*)_$""".r split_lines(File.read(llncs_dir + readme)) .collectFirst({ case Version(v) => v }) .getOrElse(error("Failed to detect version in " + readme)) } 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) /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_LLNCS_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is the Springer LaTeX LNCS style for authors from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } } } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_llncs", "build component for Springer LaTeX LNCS style", Scala_Project.here, { args => var target_dir = Path.current var download_url = default_url val getopts = Getopts(""" Usage: isabelle build_llncs [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") Build component for Springer LaTeX LNCS style. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => download_url = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_llncs(download_url = download_url, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_pdfjs.scala b/src/Pure/Admin/build_pdfjs.scala --- a/src/Pure/Admin/build_pdfjs.scala +++ b/src/Pure/Admin/build_pdfjs.scala @@ -1,102 +1,98 @@ /* Title: Pure/Admin/build_pdfjs.scala Author: Makarius Build Isabelle component for Mozilla PDF.js. See also: - https://github.com/mozilla/pdf.js - https://github.com/mozilla/pdf.js/releases - https://github.com/mozilla/pdf.js/wiki/Setup-PDF.js-in-a-website */ package isabelle object Build_PDFjs { /* build pdfjs component */ val default_url = "https://github.com/mozilla/pdf.js/releases/download" val default_version = "2.14.305" def build_pdfjs( base_url: String = default_url, version: String = default_version, target_dir: Path = Path.current, progress: Progress = new Progress ): Unit = { - Isabelle_System.require_command("unzip", test = "-h") - - /* component name */ val component = "pdfjs-" + version val component_dir = Components.Directory.create(target_dir + Path.basic(component), progress = progress) /* download */ val download_url = base_url + "/v" + version Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file => Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-legacy-dist.zip", archive_file, progress = progress) - Isabelle_System.bash("unzip -x " + File.bash_path(archive_file), - cwd = component_dir.path.file).check + Isabelle_System.extract(archive_file, component_dir.path) } /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_PDFJS_HOME="$COMPONENT" """) /* README */ File.write(component_dir.README, """This is PDF.js from """ + download_url + """ Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("build_pdfjs", "build component for Mozilla PDF.js", Scala_Project.here, { args => var target_dir = Path.current var base_url = default_url var version = default_version val getopts = Getopts(""" Usage: isabelle build_pdfjs [OPTIONS] Options are: -D DIR target directory (default ".") -U URL download URL (default: """" + default_url + """") -V VERSION version (default: """" + default_version + """") Build component for PDF.js. """, "D:" -> (arg => target_dir = Path.explode(arg)), "U:" -> (arg => base_url = arg), "V:" -> (arg => version = arg)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_pdfjs(base_url = base_url, version = version, target_dir = target_dir, progress = progress) }) } diff --git a/src/Pure/Admin/build_polyml.scala b/src/Pure/Admin/build_polyml.scala --- a/src/Pure/Admin/build_polyml.scala +++ b/src/Pure/Admin/build_polyml.scala @@ -1,266 +1,260 @@ /* Title: Pure/Admin/build_polyml.scala Author: Makarius Build Poly/ML from sources. */ package isabelle import scala.util.matching.Regex object Build_PolyML { /** platform-specific build **/ sealed case class Platform_Info( options: List[String] = Nil, setup: String = "", libs: Set[String] = Set.empty) private val platform_info = Map( "linux" -> Platform_Info( options = List("LDFLAGS=-Wl,-rpath,_DUMMY_"), libs = Set("libgmp")), "darwin" -> Platform_Info( options = List("CFLAGS=-O3", "CXXFLAGS=-O3", "LDFLAGS=-segprot POLY rwx rwx"), setup = "PATH=/usr/bin:/bin:/usr/sbin:/sbin", libs = Set("libpolyml", "libgmp")), "windows" -> Platform_Info( options = List("--host=x86_64-w64-mingw32", "CPPFLAGS=-I/mingw64/include", "--disable-windows-gui"), setup = MinGW.environment_export, libs = Set("libgcc_s_seh", "libgmp", "libstdc++", "libwinpthread"))) def build_polyml( root: Path, sha1_root: Option[Path] = None, progress: Progress = new Progress, arch_64: Boolean = false, options: List[String] = Nil, mingw: MinGW = MinGW.none ): Unit = { if (!((root + Path.explode("configure")).is_file && (root + Path.explode("PolyML")).is_dir)) error("Bad Poly/ML root directory: " + root) val platform = Isabelle_Platform.self val polyml_platform = (if (arch_64) platform.arch_64 else platform.arch_64_32) + "-" + platform.os_name val sha1_platform = platform.arch_64 + "-" + platform.os_name val info = platform_info.getOrElse(platform.os_name, error("Bad OS platform: " + quote(platform.os_name))) if (platform.is_linux) Isabelle_System.require_command("chrpath") /* bash */ def bash( cwd: Path, script: String, redirect: Boolean = false, echo: Boolean = false ): Process_Result = { val script1 = if (platform.is_arm && platform.is_macos) { "arch -arch arm64 bash -c " + Bash.string(script) } else mingw.bash_script(script) progress.bash(script1, cwd = cwd.file, redirect = redirect, echo = echo) } /* configure and make */ val configure_options = List("--disable-shared", "--enable-intinf-as-int", "--with-gmp") ::: info.options ::: options ::: (if (arch_64) Nil else List("--enable-compact32bit")) bash(root, info.setup + "\n" + """ [ -f Makefile ] && make distclean { ./configure --prefix="$PWD/target" """ + Bash.strings(configure_options) + """ rm -rf target make && make install } || { echo "Build failed" >&2; exit 2; } """, redirect = true, echo = true).check /* sha1 library */ val sha1_files = if (sha1_root.isDefined) { val dir1 = sha1_root.get bash(dir1, "./build " + sha1_platform, redirect = true, echo = true).check val dir2 = dir1 + Path.explode(sha1_platform) File.read_dir(dir2).map(entry => dir2 + Path.basic(entry)) } else Nil /* install */ val platform_dir = Path.explode(polyml_platform) Isabelle_System.rm_tree(platform_dir) Isabelle_System.make_directory(platform_dir) for (file <- sha1_files) Isabelle_System.copy_file(file, platform_dir) for { d <- List("target/bin", "target/lib") dir = root + Path.explode(d) entry <- File.read_dir(dir) } Isabelle_System.move_file(dir + Path.explode(entry), platform_dir) Executable.libraries_closure( platform_dir + Path.basic("poly").platform_exe, mingw = mingw, filter = info.libs) /* polyc: directory prefix */ val Header = "#! */bin/sh".r File.change_lines(platform_dir + Path.explode("polyc")) { case Header() :: lines => val lines1 = lines.map(line => if (line.startsWith("prefix=")) "prefix=\"$(cd \"$(dirname \"$0\")\"; pwd)\"" else if (line.startsWith("BINDIR=")) "BINDIR=\"$prefix\"" else if (line.startsWith("LIBDIR=")) "LIBDIR=\"$prefix\"" else line) "#!/usr/bin/env bash" :: lines1 case lines => error(cat_lines("Cannot patch polyc -- undetected header:" :: lines.take(3))) } } /** skeleton for component **/ private def extract_sources(source_archive: Path, component_dir: Path): Unit = { - if (source_archive.get_ext == "zip") { - Isabelle_System.bash( - "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check - } - else { - Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check - } + Isabelle_System.extract(source_archive, component_dir) val src_dir = component_dir + Path.explode("src") File.read_dir(component_dir) match { case List(s) => Isabelle_System.move_file(component_dir + Path.basic(s), src_dir) case _ => error("Source archive contains multiple directories") } val lines = split_lines(File.read(src_dir + Path.explode("RootX86.ML"))) val ml_files = for { line <- lines rest <- Library.try_unprefix("use", line) } yield "ML_file" + rest File.write(src_dir + Path.explode("ROOT.ML"), """(* Poly/ML Compiler root file. When this file is open in the Prover IDE, the ML files of the Poly/ML compiler can be explored interactively. This is a separate copy: it does not affect the running ML session. *) """ + ml_files.mkString("\n", "\n", "\n")) } def build_polyml_component( source_archive: Path, component_path: Path, sha1_root: Option[Path] = None ): Unit = { val component_dir = Components.Directory.create(component_path) extract_sources(source_archive, component_path) Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), component_dir.etc) Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/README"), component_dir.path) sha1_root match { case Some(dir) => Mercurial.repository(dir) .archive(File.standard_path(component_dir.path + Path.explode("sha1"))) case None => } } /** Isabelle tool wrappers **/ val isabelle_tool1 = Isabelle_Tool("build_polyml", "build Poly/ML from sources", Scala_Project.here, { args => var mingw = MinGW.none var arch_64 = false var sha1_root: Option[Path] = None val getopts = Getopts(""" Usage: isabelle build_polyml [OPTIONS] ROOT [CONFIGURE_OPTIONS] Options are: -M DIR msys/mingw root specification for Windows -m ARCH processor architecture (32 or 64, default: """ + (if (arch_64) "64" else "32") + """) -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 Build Poly/ML in the ROOT directory of its sources, with additional CONFIGURE_OPTIONS (e.g. --without-gmp). """, "M:" -> (arg => mingw = MinGW(Path.explode(arg))), "m:" -> { case "32" => arch_64 = false case "64" => arch_64 = true case bad => error("Bad processor architecture: " + quote(bad)) }, "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) val more_args = getopts(args) val (root, options) = more_args match { case root :: options => (Path.explode(root), options) case Nil => getopts.usage() } build_polyml(root, sha1_root = sha1_root, progress = new Console_Progress, arch_64 = arch_64, options = options, mingw = mingw) }) val isabelle_tool2 = Isabelle_Tool("build_polyml_component", "make skeleton for Poly/ML component", Scala_Project.here, { args => var sha1_root: Option[Path] = None val getopts = Getopts(""" Usage: isabelle build_polyml_component [OPTIONS] SOURCE_ARCHIVE COMPONENT_DIR Options are: -s DIR sha1 sources, see https://isabelle.sketis.net/repos/sha1 Make skeleton for Poly/ML component, based on official source archive (zip or tar.gz). """, "s:" -> (arg => sha1_root = Some(Path.explode(arg)))) val more_args = getopts(args) val (source_archive, component_dir) = more_args match { case List(archive, dir) => (Path.explode(archive), Path.explode(dir)) case _ => getopts.usage() } build_polyml_component(source_archive, component_dir, sha1_root = sha1_root) }) } diff --git a/src/Pure/System/isabelle_system.scala b/src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala +++ b/src/Pure/System/isabelle_system.scala @@ -1,515 +1,524 @@ /* Title: Pure/System/isabelle_system.scala Author: Makarius Miscellaneous Isabelle system operations. */ package isabelle import java.util.{Map => JMap, HashMap} 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 object Isabelle_System { /* settings environment */ def settings(putenv: List[(String, String)] = Nil): JMap[String, String] = { val env0 = isabelle.setup.Environment.settings() if (putenv.isEmpty) env0 else { val env = new HashMap(env0) for ((a, b) <- putenv) env.put(a, b) env } } def getenv(name: String, env: JMap[String, String] = settings()): String = Option(env.get(name)).getOrElse("") def getenv_strict(name: String, env: JMap[String, String] = settings()): String = proper_string(getenv(name, env)) getOrElse error("Undefined Isabelle environment variable: " + quote(name)) /* services */ type Service = Classpath.Service @volatile private var _classpath: Option[Classpath] = None def classpath(): Classpath = { if (_classpath.isEmpty) init() // unsynchronized check _classpath.get } def make_services[C](c: Class[C]): List[C] = classpath().make_services(c) /* init settings + classpath */ def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = { isabelle.setup.Environment.init(isabelle_root, cygwin_root) synchronized { if (_classpath.isEmpty) _classpath = Some(Classpath()) } } /* getetc -- static distribution parameters */ def getetc(name: String, root: Path = Path.ISABELLE_HOME): Option[String] = { val path = root + Path.basic("etc") + Path.basic(name) if (path.is_file) { Library.trim_split_lines(File.read(path)) match { case Nil => None case List(s) => Some(s) case _ => error("Single line expected in " + path.absolute) } } else None } /* Isabelle distribution identification */ def isabelle_id(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_ID", root = root) orElse Mercurial.archive_id(root) orElse Mercurial.id_repository(root, rev = "") getOrElse error("Failed to identify Isabelle distribution " + root.expand) object Isabelle_Id extends Scala.Fun_String("isabelle_id") { val here = Scala_Project.here def apply(arg: String): String = isabelle_id() } def isabelle_tags(root: Path = Path.ISABELLE_HOME): String = getetc("ISABELLE_TAGS", root = root) orElse Mercurial.archive_tags(root) getOrElse { if (Mercurial.is_repository(root)) { val hg = Mercurial.repository(root) hg.tags(rev = hg.parent()) } else "" } def export_isabelle_identifier(isabelle_identifier: String): String = "export ISABELLE_IDENTIFIER=" + Bash.string(isabelle_identifier) + "\n" def isabelle_identifier(): Option[String] = proper_string(getenv("ISABELLE_IDENTIFIER")) def isabelle_heading(): String = isabelle_identifier() match { case None => "" case Some(version) => " (" + version + ")" } def isabelle_name(): String = getenv_strict("ISABELLE_NAME") def identification(): String = "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading() /** file-system operations **/ /* scala functions */ private def apply_paths( args: List[String], fun: PartialFunction[List[Path], Unit] ): List[String] = { fun(args.map(Path.explode)) Nil } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = apply_paths(args, { case List(path) => fun(path) }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) /* permissions */ def chmod(arg: String, path: Path): Unit = bash("chmod " + arg + " " + File.bash_path(path)).check def chown(arg: String, path: Path): Unit = bash("chown " + arg + " " + File.bash_path(path)).check /* directories */ def make_directory(path: Path): Path = { if (!path.is_dir) { try { Files.createDirectories(path.java_path) } catch { case ERROR(_) => error("Failed to create directory: " + path.absolute) } } path } def new_directory(path: Path): Path = if (path.is_dir) error("Directory already exists: " + path.absolute) else make_directory(path) def copy_dir(dir1: Path, dir2: Path): Unit = { val res = bash("cp -a " + File.bash_path(dir1) + " " + File.bash_path(dir2)) if (!res.ok) { cat_error("Failed to copy directory " + dir1.absolute + " to " + dir2.absolute, res.err) } } def with_copy_dir[A](dir1: Path, dir2: Path)(body: => A): A = { if (dir2.is_file || dir2.is_dir) error("Directory already exists: " + dir2.absolute) else { try { copy_dir(dir1, dir2); body } finally { rm_tree(dir2 ) } } } object Make_Directory extends Scala.Fun_Strings("make_directory") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, make_directory) } object Copy_Dir extends Scala.Fun_Strings("copy_dir") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_dir) } /* copy files */ def copy_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) { try { Files.copy(src.toPath, target.toPath, StandardCopyOption.COPY_ATTRIBUTES, StandardCopyOption.REPLACE_EXISTING) } catch { case ERROR(msg) => cat_error("Failed to copy file " + File.path(src).absolute + " to " + File.path(dst).absolute, msg) } } } def copy_file(src: Path, dst: Path): Unit = copy_file(src.file, dst.file) def copy_file_base(base_dir: Path, src: Path, target_dir: Path): Unit = { val src1 = src.expand val src1_dir = src1.dir if (!src1.starts_basic) error("Illegal path specification " + src1 + " beyond base directory") copy_file(base_dir + src1, Isabelle_System.make_directory(target_dir + src1_dir)) } object Copy_File extends Scala.Fun_Strings("copy_file") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths2(args, copy_file) } object Copy_File_Base extends Scala.Fun_Strings("copy_file_base") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths3(args, copy_file_base) } /* move files */ def move_file(src: JFile, dst: JFile): Unit = { val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst if (!File.eq(src, target)) Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING) } def move_file(src: Path, dst: Path): Unit = move_file(src.file, dst.file) /* symbolic link */ def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit = { val src_file = src.file val dst_file = dst.file val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file if (force) target.delete def cygwin_link(): Unit = { if (native) { error("Failed to create native symlink on Windows: " + quote(src_file.toString) + "\n(but it could work as Administrator)") } else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target) } try { Files.createSymbolicLink(target.toPath, src_file.toPath) } catch { case _: UnsupportedOperationException if Platform.is_windows => cygwin_link() case _: FileSystemException if Platform.is_windows => cygwin_link() } } /* tmp files */ def isabelle_tmp_prefix(): JFile = { val path = Path.explode("$ISABELLE_TMP_PREFIX") path.file.mkdirs // low-level mkdirs to avoid recursion via Isabelle environment File.platform_file(path) } def tmp_file( name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix(), initialized: Boolean = true ): JFile = { val suffix = if (ext == "") "" else "." + ext val file = Files.createTempFile(base_dir.toPath, name, suffix).toFile if (initialized) file.deleteOnExit() else file.delete() file } def with_tmp_file[A]( name: String, ext: String = "", base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val file = tmp_file(name, ext, base_dir = base_dir) try { body(File.path(file)) } finally { file.delete } } /* tmp dirs */ def rm_tree(root: JFile): Unit = { root.delete if (root.isDirectory) { Files.walkFileTree(root.toPath, new SimpleFileVisitor[JPath] { override def visitFile(file: JPath, attrs: BasicFileAttributes): FileVisitResult = { try { Files.deleteIfExists(file) } catch { case _: IOException => } FileVisitResult.CONTINUE } override def postVisitDirectory(dir: JPath, e: IOException): FileVisitResult = { if (e == null) { try { Files.deleteIfExists(dir) } catch { case _: IOException => } FileVisitResult.CONTINUE } else throw e } } ) } } def rm_tree(root: Path): Unit = rm_tree(root.file) object Rm_Tree extends Scala.Fun_Strings("rm_tree") { val here = Scala_Project.here def apply(args: List[String]): List[String] = apply_paths1(args, rm_tree) } def tmp_dir(name: String, base_dir: JFile = isabelle_tmp_prefix()): JFile = { val dir = Files.createTempDirectory(base_dir.toPath, name).toFile dir.deleteOnExit() dir } def with_tmp_dir[A]( name: String, base_dir: JFile = isabelle_tmp_prefix() )(body: Path => A): A = { val dir = tmp_dir(name, base_dir = base_dir) try { body(File.path(dir)) } finally { rm_tree(dir) } } /* quasi-atomic update of directory */ def update_directory(dir: Path, f: Path => Unit): Unit = { val new_dir = dir.ext("new") val old_dir = dir.ext("old") rm_tree(new_dir) rm_tree(old_dir) f(new_dir) if (dir.is_dir) move_file(dir, old_dir) move_file(new_dir, dir) rm_tree(old_dir) } /* TCP/IP ports */ def local_port(): Int = { val socket = new ServerSocket(0) val port = socket.getLocalPort socket.close() port } /* JVM shutdown hook */ def create_shutdown_hook(body: => Unit): Thread = { val shutdown_hook = Isabelle_Thread.create(new Runnable { def run: Unit = body }) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } shutdown_hook } def remove_shutdown_hook(shutdown_hook: Thread): Unit = try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } /** external processes **/ /* GNU bash */ def bash(script: String, description: String = "", cwd: JFile = null, env: JMap[String, String] = settings(), redirect: Boolean = false, input: String = "", progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), watchdog: Option[Bash.Watchdog] = None, strict: Boolean = true, cleanup: () => Unit = () => () ): Process_Result = { Bash.process(script, description = description, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup). result(input = input, progress_stdout = progress_stdout, progress_stderr = progress_stderr, watchdog = watchdog, strict = strict) } /* command-line tools */ def require_command(cmd: String, test: String = "--version"): Unit = { if (!bash(Bash.string(cmd) + " " + test).ok) error("Missing system command: " + quote(cmd)) } private lazy val gnutar_check: Boolean = try { bash("tar --version").check.out.containsSlice("GNU tar") || error("") } catch { case ERROR(_) => false } def gnutar( args: String, dir: Path = Path.current, original_owner: Boolean = false, strip: Int = 0, redirect: Boolean = false ): Process_Result = { val options = (if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") + (if (original_owner) "" else "--owner=root --group=staff ") + (if (strip <= 0) "" else "--strip-components=" + strip + " ") if (gnutar_check) bash("tar " + options + args, redirect = redirect) else error("Expected to find GNU tar executable") } + def extract(archive: Path, dir: Path): Unit = + archive.get_ext match { + case "zip" => + Isabelle_System.bash("unzip -x " + File.bash_path(archive.absolute), cwd = dir.file).check + case "tar.gz" | "tgz" => + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check + case _ => error("Cannot extract " + archive) + } + def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = { with_tmp_file("patch") { patch => Isabelle_System.bash( "diff -ru " + diff_options + " -- " + File.bash_path(src) + " " + File.bash_path(dst) + " > " + File.bash_path(patch), cwd = base_dir.file).check_rc(_ <= 1) File.read(patch) } } def hostname(): String = bash("hostname -s").check.out def open(arg: String): Unit = bash("exec \"$ISABELLE_OPEN\" " + Bash.string(arg) + " >/dev/null 2>/dev/null &") def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" " + File.bash_path(arg) + " >/dev/null 2>/dev/null &") def open_external_file(name: String): Boolean = { val ext = Library.take_suffix((c: Char) => c != '.', name.toList)._2.mkString val external = ext.nonEmpty && Library.space_explode(':', getenv("ISABELLE_EXTERNAL_FILES")).contains(ext) if (external) { if (ext == "pdf" && Path.is_wellformed(name)) pdf_viewer(Path.explode(name)) else open(name) } external } /** Isabelle resources **/ /* repository clone with Admin */ def admin(): Boolean = Path.explode("~~/Admin").is_dir /* default logic */ def default_logic(args: String*): String = { args.find(_ != "") match { case Some(logic) => logic case None => getenv_strict("ISABELLE_LOGIC") } } /* download file */ def download(url_name: String, progress: Progress = new Progress): HTTP.Content = { val url = Url(url_name) progress.echo("Getting " + quote(url_name)) try { HTTP.Client.get(url) } catch { case ERROR(msg) => cat_error("Failed to download " + quote(url_name), msg) } } def download_file(url_name: String, file: Path, progress: Progress = new Progress): Unit = Bytes.write(file, download(url_name, progress = progress).bytes) object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = args.map(url => download(url.text).bytes) } /* repositories */ val isabelle_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/isabelle") val afp_repository: Mercurial.Server = Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel") def official_releases(): List[String] = Library.trim_split_lines( isabelle_repository.read_file(Path.explode("Admin/Release/official"))) } diff --git a/src/Tools/VSCode/src/build_vscodium.scala b/src/Tools/VSCode/src/build_vscodium.scala --- a/src/Tools/VSCode/src/build_vscodium.scala +++ b/src/Tools/VSCode/src/build_vscodium.scala @@ -1,476 +1,469 @@ /* Title: Tools/VSCode/src/build_vscodium.scala Author: Makarius Build the Isabelle system component for VSCodium: cross-compilation for all platforms. */ package isabelle.vscode import isabelle._ import java.security.MessageDigest import java.util.Base64 object Build_VSCodium { /* global parameters */ lazy val version: String = Isabelle_System.getenv_strict("ISABELLE_VSCODE_VERSION") val vscodium_repository = "https://github.com/VSCodium/vscodium.git" val vscodium_download = "https://github.com/VSCodium/vscodium/releases/download" private val resources = Path.explode("resources") /* Isabelle symbols (static subset only) */ def make_symbols(): File.Content = { val symbols = Symbol.Symbols.load(static = true) val symbols_js = JSON.Format.pretty_print( for (entry <- symbols.entries) yield JSON.Object( "symbol" -> entry.symbol, "name" -> entry.name, "abbrevs" -> entry.abbrevs) ++ JSON.optional("code", entry.code)) File.content(Path.explode("symbols.json"), symbols_js) } def make_isabelle_encoding(header: String): File.Content = { val symbols = Symbol.Symbols.load(static = true) val symbols_js = JSON.Format.pretty_print( for (entry <- symbols.entries; code <- entry.code) yield JSON.Object("symbol" -> entry.symbol, "code" -> code)) val path = Path.explode("isabelle_encoding.ts") val body = File.read(Path.explode("$ISABELLE_VSCODE_HOME/patches") + path) .replace("[/*symbols*/]", symbols_js) File.content(path, header + "\n" + body) } /* platform info */ sealed case class Platform_Info( platform: Platform.Family.Value, download_template: String, build_name: String, env: List[String] ) { 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 = { - if (download_zip) Isabelle_System.require_command("unzip", test = "-h") - Isabelle_System.with_tmp_file("download") { download_file => Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name, download_file, progress = progress) progress.echo("Extract ...") - if (download_zip) { - Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check - } - else { - Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check - } + Isabelle_System.extract(download_file, dir) } } def get_vscodium_repository(build_dir: Path, progress: Progress = new Progress): Unit = { progress.echo("Getting VSCodium repository ...") Isabelle_System.bash( List( "set -e", "git clone -n " + Bash.string(vscodium_repository) + " .", "git checkout -q " + Bash.string(version) ).mkString("\n"), cwd = build_dir.file).check progress.echo("Getting VSCode repository ...") Isabelle_System.bash(environment + "\n" + "./get_repo.sh", cwd = build_dir.file).check } def platform_dir(dir: Path): Path = { val platform_name = if (platform == Platform.Family.windows) Platform.Family.native(platform) else Platform.Family.standard(platform) dir + Path.explode(platform_name) } def build_dir(dir: Path): Path = dir + Path.explode(build_name) def environment: String = (("MS_TAG=" + Bash.string(version)) :: "SHOULD_BUILD=yes" :: "VSCODE_ARCH=x64" :: env) .map(s => "export " + s + "\n").mkString def patch_sources(base_dir: Path): String = { val dir = base_dir + Path.explode("vscode") Isabelle_System.with_copy_dir(dir, dir.orig) { // macos icns for (name <- Seq("build/lib/electron.js", "build/lib/electron.ts")) { File.change(dir + Path.explode(name), strict = true) { _.replace("""'resources/darwin/' + icon + '.icns'""", """'resources/darwin/' + icon.toLowerCase() + '.icns'""") } } // isabelle_encoding.ts { val common_dir = dir + Path.explode("src/vs/workbench/services/textfile/common") val header = split_lines(File.read(common_dir + Path.explode("encoding.ts"))) .takeWhile(_.trim.nonEmpty) make_isabelle_encoding(cat_lines(header)).write(common_dir) } // explicit patches { val patches_dir = Path.explode("$ISABELLE_VSCODE_HOME/patches") for (name <- Seq("cli", "isabelle_encoding", "no_ocaml_icons")) { val path = patches_dir + Path.explode(name).patch Isabelle_System.bash("patch -p1 < " + File.bash_path(path), cwd = dir.file).check } } Isabelle_System.make_patch(base_dir, dir.base.orig, dir.base) } } def patch_resources(base_dir: Path): String = { val dir = base_dir + resources val patch = Isabelle_System.with_copy_dir(dir, dir.orig) { val fonts_dir = dir + Path.explode("app/out/vs/base/browser/ui/fonts") HTML.init_fonts(fonts_dir.dir) make_symbols().write(fonts_dir) val workbench_css = dir + Path.explode("app/out/vs/workbench/workbench.desktop.main.css") val checksum1 = file_checksum(workbench_css) File.append(workbench_css, "\n\n" + HTML.fonts_css_dir(prefix = "../base/browser/ui")) val checksum2 = file_checksum(workbench_css) val file_name = workbench_css.file_name File.change_lines(dir + Path.explode("app/product.json")) { _.map(line => if (line.containsSlice(file_name) && line.contains(checksum1)) { line.replace(checksum1, checksum2) } else line) } Isabelle_System.make_patch(dir.dir, dir.orig.base, dir.base) } val app_dir = dir + Path.explode("app") val vscodium_app_dir = dir + Path.explode("vscodium") Isabelle_System.move_file(app_dir, vscodium_app_dir) Isabelle_System.make_directory(app_dir) if ((vscodium_app_dir + resources).is_dir) { Isabelle_System.copy_dir(vscodium_app_dir + resources, app_dir) } patch } def init_resources(base_dir: Path): Path = { val dir = base_dir + resources if (platform == Platform.Family.macos) { Isabelle_System.symlink(Path.explode("VSCodium.app/Contents/Resources"), dir) } dir } def setup_node(target_dir: Path, progress: Progress): Unit = { Isabelle_System.with_tmp_dir("download") { download_dir => download(download_dir, progress = progress) val dir1 = init_resources(download_dir) val dir2 = init_resources(target_dir) for (name <- Seq("app/node_modules.asar", "app/node_modules.asar.unpacked")) { val path = Path.explode(name) Isabelle_System.rm_tree(dir2 + path) Isabelle_System.copy_dir(dir1 + path, dir2 + path) } } } def setup_electron(dir: Path): Unit = { val electron = Path.explode("electron") platform match { case Platform.Family.linux | Platform.Family.linux_arm => Isabelle_System.move_file(dir + Path.explode("codium"), dir + electron) case Platform.Family.windows => Isabelle_System.move_file(dir + Path.explode("VSCodium.exe"), dir + electron.exe) Isabelle_System.move_file( dir + Path.explode("VSCodium.VisualElementsManifest.xml"), dir + Path.explode("electron.VisualElementsManifest.xml")) case Platform.Family.macos => } } def setup_executables(dir: Path): Unit = { Isabelle_System.rm_tree(dir + Path.explode("bin")) if (platform == Platform.Family.windows) { val files = File.find_files(dir.file, pred = { file => val name = file.getName File.is_dll(name) || File.is_exe(name) || File.is_node(name) }) files.foreach(file => File.set_executable(File.path(file), true)) Isabelle_System.bash("chmod -R o-w " + File.bash_path(dir)).check } } } // see https://github.com/microsoft/vscode/blob/main/build/gulpfile.vscode.js // function computeChecksum(filename) private def file_checksum(path: Path): String = { val digest = MessageDigest.getInstance("MD5") digest.update(Bytes.read(path).array) Bytes(Base64.getEncoder.encode(digest.digest())) .text.replaceAll("=", "") } private val platform_infos: Map[Platform.Family.Value, Platform_Info] = Iterator( Platform_Info(Platform.Family.linux, "linux-x64-{VERSION}.tar.gz", "VSCode-linux-x64", List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True")), Platform_Info(Platform.Family.linux_arm, "linux-arm64-{VERSION}.tar.gz", "VSCode-linux-arm64", List("OS_NAME=linux", "SKIP_LINUX_PACKAGES=True", "VSCODE_ARCH=arm64")), Platform_Info(Platform.Family.macos, "darwin-x64-{VERSION}.zip", "VSCode-darwin-x64", List("OS_NAME=osx")), Platform_Info(Platform.Family.windows, "win32-x64-{VERSION}.zip", "VSCode-win32-x64", List("OS_NAME=windows", "SHOULD_BUILD_ZIP=no", "SHOULD_BUILD_EXE_SYS=no", "SHOULD_BUILD_EXE_USR=no", "SHOULD_BUILD_MSI=no", "SHOULD_BUILD_MSI_NOUP=no"))) .map(info => info.platform -> info).toMap def the_platform_info(platform: Platform.Family.Value): Platform_Info = platform_infos.getOrElse(platform, error("No platform info for " + quote(platform.toString))) def linux_platform_info: Platform_Info = the_platform_info(Platform.Family.linux) /* check system */ def check_system(platforms: List[Platform.Family.Value]): Unit = { if (Platform.family != Platform.Family.linux) error("Not a Linux/x86_64 system") Isabelle_System.require_command("git") Isabelle_System.require_command("node") Isabelle_System.require_command("yarn") Isabelle_System.require_command("jq") 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") } } /* original repository clones and patches */ def vscodium_patch(verbose: Boolean = false, progress: Progress = new Progress): String = { val platform_info = linux_platform_info check_system(List(platform_info.platform)) Isabelle_System.with_tmp_dir("build") { build_dir => platform_info.get_vscodium_repository(build_dir, progress = progress) val vscode_dir = build_dir + Path.explode("vscode") progress.echo("Prepare ...") Isabelle_System.with_copy_dir(vscode_dir, vscode_dir.orig) { progress.bash( List( "set -e", platform_info.environment, "./prepare_vscode.sh", // enforce binary diff of code.xpm "cp vscode/resources/linux/code.png vscode/resources/linux/rpm/code.xpm" ).mkString("\n"), cwd = build_dir.file, echo = verbose).check Isabelle_System.make_patch(build_dir, vscode_dir.orig.base, vscode_dir.base, diff_options = "--exclude=.git --exclude=node_modules") } } } /* build vscodium */ def default_platforms: List[Platform.Family.Value] = Platform.Family.list def build_vscodium( target_dir: Path = Path.current, platforms: List[Platform.Family.Value] = default_platforms, verbose: Boolean = false, progress: Progress = new Progress ): Unit = { check_system(platforms) /* component */ val component_name = "vscodium-" + version val component_dir = Components.Directory.create(target_dir + Path.explode(component_name), progress = progress) /* patches */ progress.echo("\n* Building patches:") val patches_dir = Isabelle_System.new_directory(component_dir.path + Path.explode("patches")) def write_patch(name: String, patch: String): Unit = File.write(patches_dir + Path.explode(name).patch, patch) write_patch("01-vscodium", vscodium_patch(verbose = verbose, progress = progress)) /* build */ for (platform <- platforms) yield { val platform_info = the_platform_info(platform) Isabelle_System.with_tmp_dir("build") { build_dir => progress.echo("\n* Building " + platform + ":") platform_info.get_vscodium_repository(build_dir, progress = progress) val sources_patch = platform_info.patch_sources(build_dir) if (platform_info.is_linux) write_patch("02-isabelle_sources", sources_patch) progress.echo("Build ...") progress.bash(platform_info.environment + "\n" + "./build.sh", cwd = build_dir.file, echo = verbose).check if (platform_info.is_linux) { Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path) } val platform_dir = platform_info.platform_dir(component_dir.path) Isabelle_System.copy_dir(platform_info.build_dir(build_dir), platform_dir) platform_info.setup_node(platform_dir, progress) platform_info.setup_electron(platform_dir) val resources_patch = platform_info.patch_resources(platform_dir) if (platform_info.is_linux) write_patch("03-isabelle_resources", resources_patch) Isabelle_System.copy_file( build_dir + Path.explode("vscode/node_modules/electron/dist/resources/default_app.asar"), platform_dir + resources) platform_info.setup_executables(platform_dir) } } Isabelle_System.bash("gzip *.patch", cwd = patches_dir.file).check /* settings */ File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript: ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/MacOS/Electron" ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/VSCodium.app/Contents/Resources" else ISABELLE_VSCODIUM_ELECTRON="$ISABELLE_VSCODIUM_HOME/electron" ISABELLE_VSCODIUM_RESOURCES="$ISABELLE_VSCODIUM_HOME/resources" fi """) /* README */ File.write(component_dir.README, "This is VSCodium " + version + " from " + vscodium_repository + """ It has been built from sources using "isabelle build_vscodium". This applies a few changes required for Isabelle/VSCode, see "patches" directory for a formal record. Makarius """ + Date.Format.date(Date.now()) + "\n") } /* Isabelle tool wrappers */ val isabelle_tool1 = Isabelle_Tool("build_vscodium", "build component for VSCodium", Scala_Project.here, { args => var target_dir = Path.current var platforms = default_platforms var verbose = false val getopts = Getopts(""" Usage: build_vscodium [OPTIONS] Options are: -D DIR target directory (default ".") -p NAMES platform families (default: """ + quote(platforms.mkString(",")) + """) -v verbose Build VSCodium from sources and turn it into an Isabelle component. The build platform needs to be Linux with nodejs/yarn, jq, and wine for targeting Windows. """, "D:" -> (arg => target_dir = Path.explode(arg)), "p:" -> (arg => platforms = Library.space_explode(',', arg).map(Platform.Family.parse)), "v" -> (_ => verbose = true)) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val progress = new Console_Progress() build_vscodium(target_dir = target_dir, platforms = platforms, verbose = verbose, progress = progress) }) val isabelle_tool2 = Isabelle_Tool("vscode_patch", "patch VSCode source tree", Scala_Project.here, { args => var base_dir = Path.current val getopts = Getopts(""" Usage: vscode_patch [OPTIONS] Options are: -D DIR base directory (default ".") Patch original VSCode source tree for use with Isabelle/VSCode. """, "D:" -> (arg => base_dir = Path.explode(arg))) val more_args = getopts(args) if (more_args.nonEmpty) getopts.usage() val platform_info = the_platform_info(Platform.family) platform_info.patch_sources(base_dir) }) }