# HG changeset patch # User wenzelm # Date 1659872641 -7200 # Node ID fb12433208aa201feed914142a9e2bd29ed574ce # Parent 0ab8a9177e41c3a9fd5323d7d823c9b184ddf173 tuned signature; diff -r 0ab8a9177e41 -r fb12433208aa src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sun Aug 07 12:58:59 2022 +0200 +++ b/src/Pure/Thy/export.scala Sun Aug 07 13:44:01 2022 +0200 @@ -307,7 +307,7 @@ attempts.collectFirst({ case (name, None) => name }) match { case Some(bad) => for ((_, Some(db)) <- attempts) db.close() - store.bad_database(bad) + store.error_database(bad) case None => for ((name, Some(db)) <- attempts) yield { new Session_Database(name, db) { override def close(): Unit = this.db.close() } diff -r 0ab8a9177e41 -r fb12433208aa src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Aug 07 12:58:59 2022 +0200 +++ b/src/Pure/Thy/sessions.scala Sun Aug 07 13:44:01 2022 +0200 @@ -1305,11 +1305,11 @@ } } - def bad_database(name: String): Nothing = + def error_database(name: String): Nothing = error("Missing build database for session " + quote(name)) def open_database(name: String, output: Boolean = false): SQL.Database = - try_open_database(name, output = output) getOrElse bad_database(name) + try_open_database(name, output = output) getOrElse error_database(name) def clean_output(name: String): (Boolean, Boolean) = { val relevant_db = diff -r 0ab8a9177e41 -r fb12433208aa src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sun Aug 07 12:58:59 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Sun Aug 07 13:44:01 2022 +0200 @@ -98,7 +98,7 @@ info <- store.read_build(db, session_name) } yield (theories, errors, info.return_code) result match { - case None => error("Missing build database for session " + quote(session_name)) + case None => store.error_database(session_name) case Some((used_theories, errors, rc)) => theories.filterNot(used_theories.toSet) match { case Nil => diff -r 0ab8a9177e41 -r fb12433208aa src/Pure/Tools/profiling_report.scala --- a/src/Pure/Tools/profiling_report.scala Sun Aug 07 12:58:59 2022 +0200 +++ b/src/Pure/Tools/profiling_report.scala Sun Aug 07 13:44:01 2022 +0200 @@ -19,7 +19,7 @@ using(Export.open_session_context0(store, session)) { session_context => session_context.session_db().map(db => store.read_theories(db, session)) match { - case None => error("Missing build database for session " + quote(session)) + case None => store.error_database(session) case Some(used_theories) => theories.filterNot(used_theories.toSet) match { case Nil =>