# HG changeset patch
# User wenzelm
# Date 1678977970 -3600
# Node ID daaaf59375e93cb5fdadf29291a01800386c0624
# Parent  649708f75c6f545a809d851247545609524e4fc5
tuned signature;

diff -r 649708f75c6f -r daaaf59375e9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Mar 16 15:38:32 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Mar 16 15:46:10 2023 +0100
@@ -1549,7 +1549,7 @@
 
     def prepare_output(): Unit = Isabelle_System.make_directory(output_dir + Path.basic("log"))
 
-    def clean_output(name: String): (Boolean, Boolean) = {
+    def clean_output(name: String): Option[Boolean] = {
       val relevant_db =
         database_server &&
           using_option(try_open_database(name))(init_session_info(_, name)).getOrElse(false)
@@ -1562,9 +1562,7 @@
           path = dir + file if path.is_file
         } yield path.file.delete
 
-      val relevant = relevant_db || del.nonEmpty
-      val ok = del.forall(b => b)
-      (relevant, ok)
+      if (relevant_db || del.nonEmpty) Some(del.forall(identity)) else None
     }
 
     def init_output(name: String): Unit = {
diff -r 649708f75c6f -r daaaf59375e9 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Mar 16 15:38:32 2023 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 16 15:46:10 2023 +0100
@@ -173,10 +173,10 @@
 
     if (clean_build) {
       for (name <- full_sessions.imports_descendants(full_sessions_selection)) {
-        val (relevant, ok) = store.clean_output(name)
-        if (relevant) {
-          if (ok) progress.echo("Cleaned " + name)
-          else progress.echo(name + " FAILED to clean")
+        store.clean_output(name) match {
+          case None =>
+          case Some(true) => progress.echo("Cleaned " + name)
+          case Some(false) => progress.echo(name + " FAILED to clean")
         }
       }
     }