# HG changeset patch
# User wenzelm
# Date 1668984819 -3600
# Node ID 137cec33346f0193c92fb6e619500024eecf08e7
# Parent  b30b8e23383c3751be742c5a6f769a1f6bf14779
clarified signature;

diff -r b30b8e23383c -r 137cec33346f src/Pure/Admin/build_release.scala
--- 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))
diff -r b30b8e23383c -r 137cec33346f src/Pure/System/components.scala
--- 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)) {