# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1739529386 -3600
# Node ID 69ed0333ba5f1b7fc4c656dc3231342aa0fd2b5b
# Parent  c9f845dca3504586841884453f5319d6e7fdbad7
use core.properties for Solr index meta info;

diff -r c9f845dca350 -r 69ed0333ba5f src/Tools/Find_Facts/src/solr.scala
--- a/src/Tools/Find_Facts/src/solr.scala	Fri Feb 14 11:34:25 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Fri Feb 14 11:36:26 2025 +0100
@@ -11,6 +11,8 @@
 
 import isabelle._
 
+import java.util.{Properties => JProperties}
+
 import scala.jdk.CollectionConverters._
 
 import org.apache.solr.client.solrj.embedded.EmbeddedSolrServer
@@ -346,7 +348,12 @@
   class System private[Solr](val solr_data: Path) {
     def database_dir(database: String): Path = solr_data + Path.basic(database)
 
-    def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+    def init_database(
+      database: String,
+      data: Data,
+      props: Properties.T = Nil,
+      clean: Boolean = false
+    ): Database = {
       val db_dir = database_dir(database)
 
       if (clean) Isabelle_System.rm_tree(db_dir)
@@ -354,6 +361,12 @@
       val conf_dir = db_dir + Path.basic("conf")
       if (!conf_dir.is_dir) {
         Isabelle_System.make_directory(conf_dir)
+
+        val jprops = new JProperties
+        for ((key, value) <- props) jprops.put(key, value)
+        jprops.setProperty("name", database)
+        jprops.store(File.writer((db_dir + Path.basic("core.properties")).file), null)
+
         File.write(conf_dir + Path.basic("schema.xml"), XML.string_of_body(data.schema))
         File.write(conf_dir + Path.basic("solrconfig.xml"), XML.string_of_body(data.solr_config))
         data.more_config.foreach((path, content) => File.write(conf_dir + path, content))
@@ -365,17 +378,23 @@
     def open_database(database: String): Database =
       if (!database_dir(database).is_dir) error("Missing Solr database: " + quote(database))
       else {
+        val jprops = File.read_props(database_dir(database) + Path.basic("core.properties"))
+        val props =
+          (for (key <- jprops.stringPropertyNames().iterator().asScala)
+          yield key -> jprops.getProperty(key)).toList
+
         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)
+        new Database(props, server)
       }
   }
 
-  class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {
+  class Database private[Solr](val props: Properties.T, solr: EmbeddedSolrServer)
+    extends AutoCloseable {
     override def close(): Unit = solr.close()
 
     def execute_query[A](