# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737469917 -3600
# Node ID 838ed7098c4c8316b34323e5d71d20e9f3f87911
# Parent  6f86f2751a7be23d5f7ca48cc01f765ff83138c6
clarified: Find_Facts indexes instead of Solr components;

diff -r 6f86f2751a7b -r 838ed7098c4c src/Tools/Find_Facts/etc/settings
--- a/src/Tools/Find_Facts/etc/settings	Tue Jan 21 14:36:47 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Tue Jan 21 15:31:57 2025 +0100
@@ -4,6 +4,6 @@
 FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
 
 FIND_FACTS_SOLR_DATA="$ISABELLE_HOME_USER/find_facts/solr"
-SOLR_COMPONENTS=""
+FIND_FACTS_INDEXES=""
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
diff -r 6f86f2751a7b -r 838ed7098c4c src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 14:36:47 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 15:31:57 2025 +0100
@@ -721,7 +721,14 @@
 
   /** index components **/
 
-  def find_facts_index_component(
+  def resolve_indexes(solr: Solr.System): Unit = {
+    // non-portable: only for Linux or macOS
+    for (path <- Path.split(Isabelle_System.getenv("FIND_FACTS_INDEXES"))) {
+      Isabelle_System.symlink(path.absolute, solr.solr_data, force = true)
+    }
+  }
+
+  def find_facts_index_build(
     options: Options,
     target_dir: Path = Path.current,
     progress: Progress = new Progress
@@ -729,25 +736,26 @@
     val solr = Solr.init(solr_data_dir)
     val database = options.string("find_facts_database_name")
 
-    val component = "find_facts_index-" + database
+    val component = "find_facts-" + 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)
-    component_dir.write_settings("SOLR_COMPONENTS=\"$SOLR_COMPONENTS:$COMPONENT/" + database + "\"")
+    component_dir.write_settings(
+      "FIND_FACTS_INDEXES=\"$FIND_FACTS_INDEXES:$COMPONENT/" + database + "\"")
   }
 
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool2 = Isabelle_Tool("find_facts_index_component",
+  val isabelle_tool2 = Isabelle_Tool("find_facts_index_build",
     "build Isabelle component from Find_Facts index", Scala_Project.here,
     { args =>
       var options = Options.init()
       var target_dir = Path.current
 
       val getopts = Getopts("""
-  Usage: isabelle find_facts_index_component
+  Usage: isabelle find_facts_index_build
 
     Options are:
       -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
@@ -763,7 +771,7 @@
 
       val progress = new Console_Progress()
 
-      find_facts_index_component(options, target_dir = target_dir, progress = progress)
+      find_facts_index_build(options, target_dir = target_dir, progress = progress)
     })
 
 
@@ -903,6 +911,8 @@
     val frontend = project.build_html(progress = progress)
 
     val solr = Solr.init(solr_data_dir)
+    resolve_indexes(solr)
+
     using(solr.open_database(database)) { db =>
       val stats = Find_Facts.query_stats(db, Query(Nil))
       progress.echo("Started Find_Facts with " + stats.results + " blocks, " +
diff -r 6f86f2751a7b -r 838ed7098c4c src/Tools/Find_Facts/src/solr.scala
--- a/src/Tools/Find_Facts/src/solr.scala	Tue Jan 21 14:36:47 2025 +0100
+++ b/src/Tools/Find_Facts/src/solr.scala	Tue Jan 21 15:31:57 2025 +0100
@@ -25,12 +25,6 @@
 object Solr {
   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
-    for (path <- Path.split(Isabelle_System.getenv("SOLR_COMPONENTS"))) {
-      Isabelle_System.symlink(path.absolute, solr_data, force = true)
-    }
-
     java.util.logging.LogManager.getLogManager.reset()
     new System(solr_data)
   }