clarified: application-specific $SOLR_DATA, e.g. $FIND_FACTS_SOLR_DATA;

--- a/src/Tools/Find_Facts/etc/settings	Tue Jan 21 11:17:05 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Tue Jan 21 14:36:47 2025 +0100
@@ -3,7 +3,7 @@
 FIND_FACTS_HOME="$COMPONENT"
 FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
 
-SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
+FIND_FACTS_SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
 SOLR_COMPONENTS=""
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"

--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 11:17:05 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 14:36:47 2025 +0100
@@ -112,6 +112,8 @@
 
   /** Solr data model **/
 
+  val solr_data_dir: Path = Path.explode("$FIND_FACTS_SOLR_DATA")
+
   object private_data extends Solr.Data("find_facts") {
     /* types */
 
@@ -601,6 +603,7 @@
     progress: Progress = new Progress
   ): Unit = {
     val store = Store(options)
+    val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
     val session = Session(options, Resources.bootstrap)
 
@@ -613,7 +616,7 @@
     if (sessions.isEmpty) progress.echo("Nothing to index")
     else {
       val stats =
-        using(Solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
+        using(solr.init_database(database, Find_Facts.private_data, clean = clean)) { db =>
           using(Export.open_database_context(store)) { database_context =>
             val document_info = Document_Info.read(database_context, deps, sessions)
 
@@ -723,13 +726,14 @@
     target_dir: Path = Path.current,
     progress: Progress = new Progress
   ): Unit = {
+    val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
 
     val component = "find_facts_index-" + database
     val component_dir =
       Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
 
-    Isabelle_System.copy_dir(Solr.database_dir(database), component_dir.path)
+    Isabelle_System.copy_dir(solr.database_dir(database), component_dir.path)
     component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
   }
 
@@ -898,7 +902,8 @@
 
     val frontend = project.build_html(progress = progress)
 
-    using(Solr.open_database(database)) { db =>
+    val solr = Solr.init(solr_data_dir)
+    using(solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))
       progress.echo("Started Find_Facts with " + stats.results + " blocks, " +
         stats.consts + " consts, " + stats.typs + " typs, " + stats.thms + " thms")

--- a/src/Tools/Find_Facts/src/solr.scala	Tue Jan 21 11:17:05 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Tue Jan 21 14:36:47 2025 +0100
@@ -23,7 +23,7 @@
 
 
 object Solr {
-  def init(solr_data: Path): Path = {
+  def init(solr_data: Path): System = {
     File.write(Isabelle_System.make_directory(solr_data) + Path.basic("solr.xml"), "<solr/>")
 
     // non-portable: only for Linux or macOS
@@ -32,11 +32,9 @@
     }
 
     java.util.logging.LogManager.getLogManager.reset()
-    solr_data
+    new System(solr_data)
   }
 
-  lazy val solr_data: Path = init(Path.explode("$SOLR_DATA"))
-
 
   /** query language */
 
@@ -347,32 +345,34 @@
 
   /* database */
 
-  def database_dir(database: String): Path = solr_data + Path.basic(database)
+  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 = {
-    val db_dir = database_dir(database)
+    def init_database(database: String, data: Data, clean: Boolean = false): Database = {
+      val db_dir = database_dir(database)
 
-    if (clean) Isabelle_System.rm_tree(db_dir)
+      if (clean) Isabelle_System.rm_tree(db_dir)
 
-    val conf_dir = db_dir + Path.basic("conf")
-    if (!conf_dir.is_dir) {
-      Isabelle_System.make_directory(conf_dir)
-      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))
+      val conf_dir = db_dir + Path.basic("conf")
+      if (!conf_dir.is_dir) {
+        Isabelle_System.make_directory(conf_dir)
+        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))
+      }
+
+      open_database(database)
     }
 
-    open_database(database)
-  }
-
-  def open_database(database: String): Database = {
-    val server = new EmbeddedSolrServer(solr_data.java_path, 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)
+      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(server)
+    }
   }
 
   class Database private[Solr](solr: EmbeddedSolrServer) extends AutoCloseable {