--- 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 = {
--- 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")
}
}
}