# 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 =>