--- a/src/Pure/Admin/build_release.scala Sun Nov 20 23:37:54 2022 +0100
+++ b/src/Pure/Admin/build_release.scala Sun Nov 20 23:53:39 2022 +0100
@@ -177,7 +177,7 @@
List(platform.toString, "bundled-" + platform.toString).
map((_, new Bundled(platform = Some(platform)))))
- File.append(Components.components(dir),
+ File.append(Components.Directory(dir).components,
terminate_lines("#bundled components" ::
(for {
(catalog, bundled) <- catalogs.iterator
@@ -191,7 +191,7 @@
def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = {
val Bundled = new Bundled(platform = Some(platform))
val components =
- for { Bundled(name) <- Components.read_components(dir) } yield name
+ for { Bundled(name) <- Components.Directory(dir).read_components() } yield name
val jdk_component =
components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
(components, jdk_component)
@@ -203,11 +203,12 @@
Components.contrib(name = name).implode
val Bundled = new Bundled(platform = Some(platform))
- Components.write_components(dir,
- Components.read_components(dir).flatMap(line =>
+ val component_dir = Components.Directory(dir)
+ component_dir.write_components(
+ component_dir.read_components().flatMap(line =>
line match {
case Bundled(name) =>
- if (Components.check_dir(Components.contrib(dir, name))) Some(contrib_name(name))
+ if (Components.Directory(Components.contrib(dir, name)).check) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
--- a/src/Pure/System/components.scala Sun Nov 20 23:37:54 2022 +0100
+++ b/src/Pure/System/components.scala Sun Nov 20 23:53:39 2022 +0100
@@ -125,19 +125,14 @@
def build_props: Path = etc + Path.basic("build.props")
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
- }
- 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: Boolean = settings.is_file || components.is_file
- 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))
+ def read_components(): List[String] =
+ split_lines(File.read(components)).filter(_.nonEmpty)
+ def write_components(lines: List[String]): Unit =
+ File.write(components, terminate_lines(lines))
+ }
/* component repository content */
@@ -175,7 +170,9 @@
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)
+ if (!Directory(path).check && !Sessions.is_session_dir(path)) {
+ error("Bad component directory: " + path)
+ }
val lines1 = read_components()
val lines2 =
@@ -222,9 +219,9 @@
case Archive(_) => path
case name =>
if (!path.is_dir) error("Bad component directory: " + path)
- else if (!check_dir(path)) {
+ else if (!Directory(path).check) {
error("Malformed component directory: " + path +
- "\n (requires " + settings() + " or " + Components.components() + ")")
+ "\n (requires etc/settings or etc/components)")
}
else {
val component_path = path.expand
@@ -275,7 +272,7 @@
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))
+ Directory(tmp_dir + Path.explode(name)).check
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {