# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737539600 -3600
# Node ID db9bf651701d6bb32da358247ec613f7d5d92ca9
# Parent  9d1003cb98448479e7858a44c9852f8b165a8a53
explicit error message when Solr database does not exist;

diff -r 9d1003cb9844 -r db9bf651701d src/Tools/Find_Facts/src/solr.scala
--- a/src/Tools/Find_Facts/src/solr.scala	Wed Jan 22 10:35:17 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Wed Jan 22 10:53:20 2025 +0100
@@ -358,15 +358,17 @@
       open_database(database)
     }
 
-    def open_database(database: String): Database = {
-      val server = new EmbeddedSolrServer(solr_data.java_path, database)
-
-      val cores = server.getCoreContainer.getAllCoreNames.asScala
-      if (cores.contains(database)) server.getCoreContainer.reload(database)
-      else server.getCoreContainer.create(database, Map.empty.asJava)
-
-      new Database(server)
-    }
+    def open_database(database: String): Database =
+      if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
+      else {
+        val server = new EmbeddedSolrServer(solr_data.java_path, database)
+  
+        val cores = server.getCoreContainer.getAllCoreNames.asScala
+        if (cores.contains(database)) server.getCoreContainer.reload(database)
+        else server.getCoreContainer.create(database, Map.empty.asJava)
+  
+        new Database(server)
+      }
   }
 
   class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {