# HG changeset patch # User wenzelm # Date 1622919660 -7200 # Node ID 43882e34c038db7b5b8a12575b34a4846fc622be # Parent c8b4a4f69068d1c423a12e299e16e82789c0bbdf clarified modules; diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/Admin/components.scala --- a/src/Pure/Admin/components.scala Sat Jun 05 20:20:25 2021 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,355 +0,0 @@ -/* Title: Pure/Admin/components.scala - Author: Makarius - -Isabelle system components. -*/ - -package isabelle - - -import java.io.{File => JFile} - - -object Components -{ - /* archive name */ - - object Archive - { - val suffix: String = ".tar.gz" - - def apply(name: String): String = - if (name == "") error("Bad component name: " + quote(name)) - else name + suffix - - def unapply(archive: String): Option[String] = - { - for { - name0 <- Library.try_unsuffix(suffix, archive) - name <- proper_string(name0) - } yield name - } - - def get_name(archive: String): String = - unapply(archive) getOrElse - error("Bad component archive name (expecting .tar.gz): " + quote(archive)) - } - - - /* component collections */ - - def default_component_repository: String = - Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") - - val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") - - def admin(dir: Path): Path = dir + Path.explode("Admin/components") - - def contrib(dir: Path = Path.current, name: String = ""): Path = - dir + Path.explode("contrib") + Path.explode(name) - - def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = - { - val name = Archive.get_name(archive.file_name) - progress.echo("Unpacking " + name) - Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check - name - } - - def resolve(base_dir: Path, names: List[String], - target_dir: Option[Path] = None, - copy_dir: Option[Path] = None, - progress: Progress = new Progress): Unit = - { - Isabelle_System.make_directory(base_dir) - for (name <- names) { - val archive_name = Archive(name) - val archive = base_dir + Path.explode(archive_name) - if (!archive.is_file) { - val remote = Components.default_component_repository + "/" + archive_name - Isabelle_System.download_file(remote, archive, progress = progress) - } - for (dir <- copy_dir) { - Isabelle_System.make_directory(dir) - Isabelle_System.copy_file(archive, dir) - } - unpack(target_dir getOrElse base_dir, archive, progress = progress) - } - } - - private val platforms_family: Map[Platform.Family.Value, Set[String]] = - Map( - Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), - Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), - Platform.Family.macos -> - Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), - Platform.Family.windows -> - Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) - - private val platforms_all: Set[String] = - Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) - - def purge(dir: Path, platform: Platform.Family.Value): Unit = - { - val purge_set = platforms_all -- platforms_family(platform) - - File.find_files(dir.file, - (file: JFile) => file.isDirectory && purge_set(file.getName), - include_dirs = true).foreach(Isabelle_System.rm_tree) - } - - - /* component directory content */ - - def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") - def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") - - def check_dir(dir: Path): Boolean = - settings(dir).is_file || components(dir).is_file - - def read_components(dir: Path): List[String] = - split_lines(File.read(components(dir))).filter(_.nonEmpty) - - def write_components(dir: Path, lines: List[String]): Unit = - File.write(components(dir), terminate_lines(lines)) - - - /* component repository content */ - - val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") - - sealed case class SHA1_Digest(sha1: String, file_name: String) - { - override def toString: String = sha1 + " " + file_name - } - - def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = - (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => - Word.explode(line) match { - case Nil => None - case List(sha1, name) => Some(SHA1_Digest(sha1, name)) - case _ => error("Bad components.sha1 entry: " + quote(line)) - }) - - def write_components_sha1(entries: List[SHA1_Digest]): Unit = - File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) - - - /** manage user components **/ - - val components_path = Path.explode("$ISABELLE_HOME_USER/etc/components") - - def read_components(): List[String] = - if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) - else Nil - - def write_components(lines: List[String]): Unit = - { - Isabelle_System.make_directory(components_path.dir) - File.write(components_path, Library.terminate_lines(lines)) - } - - def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = - { - val path = path0.expand.absolute - if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path) - - val lines1 = read_components() - val lines2 = - lines1.filter(line => - line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) - val lines3 = if (add) lines2 ::: List(path.implode) else lines2 - - if (lines1 != lines3) write_components(lines3) - - val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" - progress.echo(prefix + " component " + path) - } - - - /* main entry point */ - - def main(args: Array[String]): Unit = - { - Command_Line.tool { - for (arg <- args) { - val add = - if (arg.startsWith("+")) true - else if (arg.startsWith("-")) false - else error("Bad argument: " + quote(arg)) - val path = Path.explode(arg.substring(1)) - update_components(add, path, progress = new Console_Progress) - } - } - } - - - /** build and publish components **/ - - def build_components( - options: Options, - components: List[Path], - progress: Progress = new Progress, - publish: Boolean = false, - force: Boolean = false, - update_components_sha1: Boolean = false): Unit = - { - val archives: List[Path] = - for (path <- components) yield { - path.file_name match { - case Archive(_) => path - case name => - if (!path.is_dir) error("Bad component directory: " + path) - else if (!check_dir(path)) { - error("Malformed component directory: " + path + - "\n (requires " + settings() + " or " + Components.components() + ")") - } - else { - val component_path = path.expand - val archive_dir = component_path.dir - val archive_name = Archive(name) - - val archive = archive_dir + Path.explode(archive_name) - if (archive.is_file && !force) { - error("Component archive already exists: " + archive) - } - - progress.echo("Packaging " + archive_name) - Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), - dir = archive_dir).check - - archive - } - } - } - - if ((publish && archives.nonEmpty) || update_components_sha1) { - options.string("isabelle_components_server") match { - case SSH.Target(user, host) => - using(SSH.open_session(options, host = host, user = user))(ssh => - { - val components_dir = Path.explode(options.string("isabelle_components_dir")) - val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) - - for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { - error("Bad remote directory: " + dir) - } - - if (publish) { - for (archive <- archives) { - val archive_name = archive.file_name - val name = Archive.get_name(archive_name) - val remote_component = components_dir + archive.base - val remote_contrib = contrib_dir + Path.explode(name) - - // component archive - if (ssh.is_file(remote_component) && !force) { - error("Remote component archive already exists: " + remote_component) - } - progress.echo("Uploading " + archive_name) - ssh.write_file(remote_component, archive) - - // contrib directory - val is_standard_component = - Isabelle_System.with_tmp_dir("component")(tmp_dir => - { - Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check - check_dir(tmp_dir + Path.explode(name)) - }) - if (is_standard_component) { - if (ssh.is_dir(remote_contrib)) { - if (force) ssh.rm_tree(remote_contrib) - else error("Remote component directory already exists: " + remote_contrib) - } - progress.echo("Unpacking remote " + archive_name) - ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + - ssh.bash_path(remote_component)).check - } - else { - progress.echo_warning("No unpacking of non-standard component: " + archive_name) - } - } - } - - // remote SHA1 digests - if (update_components_sha1) { - val lines = - for { - entry <- ssh.read_dir(components_dir) - if entry.is_file && entry.name.endsWith(Archive.suffix) - } - yield { - progress.echo("Digesting remote " + entry.name) - ssh.execute("cd " + ssh.bash_path(components_dir) + - "; sha1sum " + Bash.string(entry.name)).check.out - } - write_components_sha1(read_components_sha1(lines)) - } - }) - case s => error("Bad isabelle_components_server: " + quote(s)) - } - } - - // local SHA1 digests - { - val new_entries = - for (archive <- archives) - yield { - val file_name = archive.file_name - progress.echo("Digesting local " + file_name) - val sha1 = SHA1.digest(archive).rep - SHA1_Digest(sha1, file_name) - } - val new_names = new_entries.map(_.file_name).toSet - - write_components_sha1( - new_entries ::: - read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) - } - } - - - /* Isabelle tool wrapper */ - - private val relevant_options = - List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") - - val isabelle_tool = - Isabelle_Tool("build_components", "build and publish Isabelle components", - Scala_Project.here, args => - { - var publish = false - var update_components_sha1 = false - var force = false - var options = Options.init() - - def show_options: String = - cat_lines(relevant_options.map(name => options.options(name).print)) - - val getopts = Getopts(""" -Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... - - Options are: - -P publish on SSH server (see options below) - -f force: overwrite existing component archives and directories - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -u update all SHA1 keys in Isabelle repository Admin/components - - Build and publish Isabelle components as .tar.gz archives on SSH server, - depending on system options: - -""" + Library.indent_lines(2, show_options) + "\n", - "P" -> (_ => publish = true), - "f" -> (_ => force = true), - "o:" -> (arg => options = options + arg), - "u" -> (_ => update_components_sha1 = true)) - - val more_args = getopts(args) - if (more_args.isEmpty && !update_components_sha1) getopts.usage() - - val progress = new Console_Progress - - build_components(options, more_args.map(Path.explode), progress = progress, - publish = publish, force = force, update_components_sha1 = update_components_sha1) - }) -} diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/System/components.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/components.scala Sat Jun 05 21:01:00 2021 +0200 @@ -0,0 +1,361 @@ +/* Title: Pure/System/components.scala + Author: Makarius + +Isabelle system components. +*/ + +package isabelle + + +import java.io.{File => JFile} + + +object Components +{ + /* archive name */ + + object Archive + { + val suffix: String = ".tar.gz" + + def apply(name: String): String = + if (name == "") error("Bad component name: " + quote(name)) + else name + suffix + + def unapply(archive: String): Option[String] = + { + for { + name0 <- Library.try_unsuffix(suffix, archive) + name <- proper_string(name0) + } yield name + } + + def get_name(archive: String): String = + unapply(archive) getOrElse + error("Bad component archive name (expecting .tar.gz): " + quote(archive)) + } + + + /* component collections */ + + def default_component_repository: String = + Isabelle_System.getenv("ISABELLE_COMPONENT_REPOSITORY") + + val default_components_base: Path = Path.explode("$ISABELLE_COMPONENTS_BASE") + + def admin(dir: Path): Path = dir + Path.explode("Admin/components") + + def contrib(dir: Path = Path.current, name: String = ""): Path = + dir + Path.explode("contrib") + Path.explode(name) + + def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = + { + val name = Archive.get_name(archive.file_name) + progress.echo("Unpacking " + name) + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check + name + } + + def resolve(base_dir: Path, names: List[String], + target_dir: Option[Path] = None, + copy_dir: Option[Path] = None, + progress: Progress = new Progress): Unit = + { + Isabelle_System.make_directory(base_dir) + for (name <- names) { + val archive_name = Archive(name) + val archive = base_dir + Path.explode(archive_name) + if (!archive.is_file) { + val remote = Components.default_component_repository + "/" + archive_name + Isabelle_System.download_file(remote, archive, progress = progress) + } + for (dir <- copy_dir) { + Isabelle_System.make_directory(dir) + Isabelle_System.copy_file(archive, dir) + } + unpack(target_dir getOrElse base_dir, archive, progress = progress) + } + } + + private val platforms_family: Map[Platform.Family.Value, Set[String]] = + Map( + Platform.Family.linux_arm -> Set("arm64-linux", "arm64_32-linux"), + Platform.Family.linux -> Set("x86_64-linux", "x86_64_32-linux"), + Platform.Family.macos -> + Set("arm64-darwin", "arm64_32-darwin", "x86_64-darwin", "x86_64_32-darwin"), + Platform.Family.windows -> + Set("x86_64-cygwin", "x86_64-windows", "x86_64_32-windows", "x86-windows")) + + private val platforms_all: Set[String] = + Set("x86-linux", "x86-cygwin") ++ platforms_family.iterator.flatMap(_._2) + + def purge(dir: Path, platform: Platform.Family.Value): Unit = + { + val purge_set = platforms_all -- platforms_family(platform) + + File.find_files(dir.file, + (file: JFile) => file.isDirectory && purge_set(file.getName), + include_dirs = true).foreach(Isabelle_System.rm_tree) + } + + + /* component directories */ + + def directories(): List[Path] = + Path.split(Isabelle_System.getenv_strict("ISABELLE_COMPONENTS")) + + + /* component directory content */ + + def settings(dir: Path = Path.current): Path = dir + Path.explode("etc/settings") + def components(dir: Path = Path.current): Path = dir + Path.explode("etc/components") + + def check_dir(dir: Path): Boolean = + settings(dir).is_file || components(dir).is_file + + def read_components(dir: Path): List[String] = + split_lines(File.read(components(dir))).filter(_.nonEmpty) + + def write_components(dir: Path, lines: List[String]): Unit = + File.write(components(dir), terminate_lines(lines)) + + + /* component repository content */ + + val components_sha1: Path = Path.explode("~~/Admin/components/components.sha1") + + sealed case class SHA1_Digest(sha1: String, file_name: String) + { + override def toString: String = sha1 + " " + file_name + } + + def read_components_sha1(lines: List[String] = Nil): List[SHA1_Digest] = + (proper_list(lines) getOrElse split_lines(File.read(components_sha1))).flatMap(line => + Word.explode(line) match { + case Nil => None + case List(sha1, name) => Some(SHA1_Digest(sha1, name)) + case _ => error("Bad components.sha1 entry: " + quote(line)) + }) + + def write_components_sha1(entries: List[SHA1_Digest]): Unit = + File.write(components_sha1, entries.sortBy(_.file_name).mkString("", "\n", "\n")) + + + /** manage user components **/ + + val components_path = Path.explode("$ISABELLE_HOME_USER/etc/components") + + def read_components(): List[String] = + if (components_path.is_file) Library.trim_split_lines(File.read(components_path)) + else Nil + + def write_components(lines: List[String]): Unit = + { + Isabelle_System.make_directory(components_path.dir) + File.write(components_path, Library.terminate_lines(lines)) + } + + def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = + { + val path = path0.expand.absolute + if (!check_dir(path) && !Sessions.is_session_dir(path)) error("Bad component directory: " + path) + + val lines1 = read_components() + val lines2 = + lines1.filter(line => + line.isEmpty || line.startsWith("#") || !File.eq(Path.explode(line), path)) + val lines3 = if (add) lines2 ::: List(path.implode) else lines2 + + if (lines1 != lines3) write_components(lines3) + + val prefix = if (lines1 == lines3) "Unchanged" else if (add) "Added" else "Removed" + progress.echo(prefix + " component " + path) + } + + + /* main entry point */ + + def main(args: Array[String]): Unit = + { + Command_Line.tool { + for (arg <- args) { + val add = + if (arg.startsWith("+")) true + else if (arg.startsWith("-")) false + else error("Bad argument: " + quote(arg)) + val path = Path.explode(arg.substring(1)) + update_components(add, path, progress = new Console_Progress) + } + } + } + + + /** build and publish components **/ + + def build_components( + options: Options, + components: List[Path], + progress: Progress = new Progress, + publish: Boolean = false, + force: Boolean = false, + update_components_sha1: Boolean = false): Unit = + { + val archives: List[Path] = + for (path <- components) yield { + path.file_name match { + case Archive(_) => path + case name => + if (!path.is_dir) error("Bad component directory: " + path) + else if (!check_dir(path)) { + error("Malformed component directory: " + path + + "\n (requires " + settings() + " or " + Components.components() + ")") + } + else { + val component_path = path.expand + val archive_dir = component_path.dir + val archive_name = Archive(name) + + val archive = archive_dir + Path.explode(archive_name) + if (archive.is_file && !force) { + error("Component archive already exists: " + archive) + } + + progress.echo("Packaging " + archive_name) + Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name), + dir = archive_dir).check + + archive + } + } + } + + if ((publish && archives.nonEmpty) || update_components_sha1) { + options.string("isabelle_components_server") match { + case SSH.Target(user, host) => + using(SSH.open_session(options, host = host, user = user))(ssh => + { + val components_dir = Path.explode(options.string("isabelle_components_dir")) + val contrib_dir = Path.explode(options.string("isabelle_components_contrib_dir")) + + for (dir <- List(components_dir, contrib_dir) if !ssh.is_dir(dir)) { + error("Bad remote directory: " + dir) + } + + if (publish) { + for (archive <- archives) { + val archive_name = archive.file_name + val name = Archive.get_name(archive_name) + val remote_component = components_dir + archive.base + val remote_contrib = contrib_dir + Path.explode(name) + + // component archive + if (ssh.is_file(remote_component) && !force) { + error("Remote component archive already exists: " + remote_component) + } + progress.echo("Uploading " + archive_name) + ssh.write_file(remote_component, archive) + + // contrib directory + val is_standard_component = + Isabelle_System.with_tmp_dir("component")(tmp_dir => + { + Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check + check_dir(tmp_dir + Path.explode(name)) + }) + if (is_standard_component) { + if (ssh.is_dir(remote_contrib)) { + if (force) ssh.rm_tree(remote_contrib) + else error("Remote component directory already exists: " + remote_contrib) + } + progress.echo("Unpacking remote " + archive_name) + ssh.execute("tar -C " + ssh.bash_path(contrib_dir) + " -xzf " + + ssh.bash_path(remote_component)).check + } + else { + progress.echo_warning("No unpacking of non-standard component: " + archive_name) + } + } + } + + // remote SHA1 digests + if (update_components_sha1) { + val lines = + for { + entry <- ssh.read_dir(components_dir) + if entry.is_file && entry.name.endsWith(Archive.suffix) + } + yield { + progress.echo("Digesting remote " + entry.name) + ssh.execute("cd " + ssh.bash_path(components_dir) + + "; sha1sum " + Bash.string(entry.name)).check.out + } + write_components_sha1(read_components_sha1(lines)) + } + }) + case s => error("Bad isabelle_components_server: " + quote(s)) + } + } + + // local SHA1 digests + { + val new_entries = + for (archive <- archives) + yield { + val file_name = archive.file_name + progress.echo("Digesting local " + file_name) + val sha1 = SHA1.digest(archive).rep + SHA1_Digest(sha1, file_name) + } + val new_names = new_entries.map(_.file_name).toSet + + write_components_sha1( + new_entries ::: + read_components_sha1().filterNot(entry => new_names.contains(entry.file_name))) + } + } + + + /* Isabelle tool wrapper */ + + private val relevant_options = + List("isabelle_components_server", "isabelle_components_dir", "isabelle_components_contrib_dir") + + val isabelle_tool = + Isabelle_Tool("build_components", "build and publish Isabelle components", + Scala_Project.here, args => + { + var publish = false + var update_components_sha1 = false + var force = false + var options = Options.init() + + def show_options: String = + cat_lines(relevant_options.map(name => options.options(name).print)) + + val getopts = Getopts(""" +Usage: isabelle build_components [OPTIONS] ARCHIVES... DIRS... + + Options are: + -P publish on SSH server (see options below) + -f force: overwrite existing component archives and directories + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -u update all SHA1 keys in Isabelle repository Admin/components + + Build and publish Isabelle components as .tar.gz archives on SSH server, + depending on system options: + +""" + Library.indent_lines(2, show_options) + "\n", + "P" -> (_ => publish = true), + "f" -> (_ => force = true), + "o:" -> (arg => options = options + arg), + "u" -> (_ => update_components_sha1 = true)) + + val more_args = getopts(args) + if (more_args.isEmpty && !update_components_sha1) getopts.usage() + + val progress = new Console_Progress + + build_components(options, more_args.map(Path.explode), progress = progress, + publish = publish, force = force, update_components_sha1 = update_components_sha1) + }) +} diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Jun 05 20:20:25 2021 +0200 +++ b/src/Pure/System/isabelle_system.scala Sat Jun 05 21:01:00 2021 +0200 @@ -581,12 +581,6 @@ def admin(): Boolean = Path.explode("~~/Admin").is_dir - /* components */ - - def components(): List[Path] = - Path.split(getenv_strict("ISABELLE_COMPONENTS")) - - /* default logic */ def default_logic(args: String*): String = diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Jun 05 20:20:25 2021 +0200 +++ b/src/Pure/System/options.scala Sat Jun 05 21:01:00 2021 +0200 @@ -134,7 +134,7 @@ { var options = empty for { - dir <- Isabelle_System.components() + dir <- Components.directories() file = dir + OPTIONS if file.is_file } { options = Parser.parse_file(options, file.implode, File.read(file)) } opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _) diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Jun 05 20:20:25 2021 +0200 +++ b/src/Pure/Thy/sessions.scala Sat Jun 05 21:01:00 2021 +0200 @@ -1023,7 +1023,7 @@ def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = { - val default_dirs = Isabelle_System.components().filter(is_session_dir) + val default_dirs = Components.directories().filter(is_session_dir) for { (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _)) } yield (select, dir.canonical) } diff -r c8b4a4f69068 -r 43882e34c038 src/Pure/build-jars --- a/src/Pure/build-jars Sat Jun 05 20:20:25 2021 +0200 +++ b/src/Pure/build-jars Sat Jun 05 21:01:00 2021 +0200 @@ -34,7 +34,6 @@ src/Pure/Admin/build_zipperposition.scala src/Pure/Admin/check_sources.scala src/Pure/Admin/ci_profile.scala - src/Pure/Admin/components.scala src/Pure/Admin/isabelle_cronjob.scala src/Pure/Admin/isabelle_devel.scala src/Pure/Admin/jenkins.scala @@ -132,6 +131,7 @@ src/Pure/ROOT.scala src/Pure/System/bash.scala src/Pure/System/command_line.scala + src/Pure/System/components.scala src/Pure/System/cygwin.scala src/Pure/System/executable.scala src/Pure/System/getopts.scala