# HG changeset patch # User Fabian Huch # 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](