clarified solr_data directory, provided via settings;
authorwenzelm
Sun, 12 Jan 2025 21:38:38 +0100
changeset 81796 88c172ebffdd
parent 81795 2856d67c8879
child 81797 d7113296c541
clarified solr_data directory, provided via settings;
NEWS
src/Tools/Find_Facts/etc/settings
src/Tools/Find_Facts/src/solr.scala
--- a/NEWS	Sun Jan 12 21:26:30 2025 +0100
+++ b/NEWS	Sun Jan 12 21:38:38 2025 +0100
@@ -357,7 +357,7 @@
     isabelle find_facts_server
     open http://localhost:8080/app#search?q=Hilbert
 
-Persistent data is stored in $ISABELLE_HOME_USER/solr/.
+Persistent data is stored in $ISABELLE_HOME_USER/find_facts/.
 
 * The Build_Manager module has replaced previous glue-code for Jenkins
 integration. The module contains a server that coordinates continuous
--- a/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:26:30 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:38:38 2025 +0100
@@ -3,4 +3,6 @@
 FIND_FACTS_HOME="$COMPONENT"
 FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
 
+SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
+
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
--- a/src/Tools/Find_Facts/src/solr.scala	Sun Jan 12 21:26:30 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Sun Jan 12 21:38:38 2025 +0100
@@ -23,17 +23,17 @@
 
 
 object Solr {
-  def init(solr_home: Path): Path = {
-    File.write(Isabelle_System.make_directory(solr_home) + Path.basic("solr.xml"), "<solr/>")
+  def init(solr_data: Path): Path = {
+    File.write(Isabelle_System.make_directory(solr_data) + Path.basic("solr.xml"), "<solr/>")
 
     for (entry <- space_explode(':', Isabelle_System.getenv("SOLR_COMPONENTS")) if entry.nonEmpty)
-      Isabelle_System.symlink(Path.explode(entry).absolute, solr_home, force = true)
+      Isabelle_System.symlink(Path.explode(entry).absolute, solr_data, force = true)
 
     java.util.logging.LogManager.getLogManager.reset()
-    solr_home
+    solr_data
   }
 
-  lazy val solr_home = init(Path.explode("$ISABELLE_HOME_USER/solr"))
+  lazy val solr_data: Path = init(Path.explode("$SOLR_DATA"))
 
 
   /** query language */
@@ -345,7 +345,7 @@
 
   /* database */
 
-  def database_dir(database: String): Path = solr_home + Path.basic(database)
+  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)
@@ -364,7 +364,7 @@
   }
 
   def open_database(database: String): Database = {
-    val server = new EmbeddedSolrServer(solr_home.java_path, database)
+    val server = new EmbeddedSolrServer(solr_data.java_path, database)
 
     val cores = server.getCoreContainer.getAllCoreNames.asScala
     if (cores.contains(database)) server.getCoreContainer.reload(database)