# HG changeset patch
# User wenzelm
# Date 1669890779 -3600
# Node ID a82fc7755ba5c0e993eb00cb3f254b10a451b155
# Parent  8f580e62ca6e4795d1139a3d79c9d849c4f044ea
clarified check;
tuned message;

diff -r 8f580e62ca6e -r a82fc7755ba5 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Dec 01 11:30:51 2022 +0100
+++ b/src/Pure/Admin/build_release.scala	Thu Dec 01 11:32:59 2022 +0100
@@ -208,7 +208,7 @@
       component_dir.read_components().flatMap(line =>
         line match {
           case Bundled(name) =>
-            if (Components.Directory(Components.contrib(dir, name)).check) Some(contrib_name(name))
+            if (Components.Directory(Components.contrib(dir, name)).ok) Some(contrib_name(name))
             else None
           case _ => if (Bundled.detect(line)) None else Some(line)
         }) ::: more_names.map(contrib_name))
diff -r 8f580e62ca6e -r a82fc7755ba5 src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Thu Dec 01 11:30:51 2022 +0100
+++ b/src/Pure/System/components.scala	Thu Dec 01 11:32:59 2022 +0100
@@ -125,7 +125,15 @@
       this
     }
 
-    def check: Boolean = settings.is_file || components.is_file
+    def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path)
+
+    def check: Directory =
+      if (!path.is_dir) error("Bad component directory: " + path)
+      else if (!ok) {
+        error("Malformed component directory: " + path +
+          "\n  (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
+      }
+      else this
 
     def read_components(): List[String] =
       split_lines(File.read(components)).filter(_.nonEmpty)
@@ -172,9 +180,7 @@
 
   def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
     val path = path0.expand.absolute
-    if (!Directory(path).check && !Sessions.is_session_dir(path)) {
-      error("Bad component directory: " + path)
-    }
+    Directory(path).check
 
     val lines1 = read_components()
     val lines2 =
@@ -220,27 +226,21 @@
         path.file_name match {
           case Archive(_) => path
           case name =>
-            if (!path.is_dir) error("Bad component directory: " + path)
-            else if (!Directory(path).check) {
-              error("Malformed component directory: " + path +
-                "\n  (requires etc/settings or etc/components)")
-            }
-            else {
-              val component_path = path.expand
-              val archive_dir = component_path.dir
-              val archive_name = Archive(name)
+            Directory(path).check
+            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)
-              }
+            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
+            progress.echo("Packaging " + archive_name)
+            Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
+              dir = archive_dir).check
 
-              archive
-            }
+            archive
         }
       }
 
@@ -274,7 +274,7 @@
             val is_standard_component =
               Isabelle_System.with_tmp_dir("component") { tmp_dir =>
                 Isabelle_System.extract(archive, tmp_dir)
-                Directory(tmp_dir + Path.explode(name)).check
+                Directory(tmp_dir + Path.explode(name)).ok
               }
             if (is_standard_component) {
               if (ssh.is_dir(remote_contrib)) {