# 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") } } }