--- 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](