tool wrappers with specific java options, notably classpath "$SOLR_JARS";
authorwenzelm
Sun, 12 Jan 2025 00:05:01 +0100
changeset 81772 c405ad565d70
parent 81771 5589ab62869e
child 81773 5df6481f45f9
tool wrappers with specific java options, notably classpath "$SOLR_JARS";
etc/build.props
src/Pure/System/isabelle_tool.scala
src/Tools/Find_Facts/Tools/find_facts
src/Tools/Find_Facts/Tools/find_facts_index
src/Tools/Find_Facts/etc/settings
src/Tools/Find_Facts/src/find_facts.scala
src/Tools/Find_Facts/src/find_facts_tools.scala
--- a/etc/build.props	Sat Jan 11 23:33:55 2025 +0100
+++ b/etc/build.props	Sun Jan 12 00:05:01 2025 +0100
@@ -252,6 +252,7 @@
   src/Pure/update.scala \
   src/Tools/Find_Facts/src/elm.scala \
   src/Tools/Find_Facts/src/find_facts.scala \
+  src/Tools/Find_Facts/src/find_facts_tools.scala \
   src/Tools/Find_Facts/src/solr.scala \
   src/Tools/Find_Facts/src/thy_blocks.scala \
   src/Tools/Graphview/graph_file.scala \
--- a/src/Pure/System/isabelle_tool.scala	Sat Jan 11 23:33:55 2025 +0100
+++ b/src/Pure/System/isabelle_tool.scala	Sun Jan 12 00:05:01 2025 +0100
@@ -208,9 +208,7 @@
   Component_Zipperposition.isabelle_tool,
   Component_Zstd.isabelle_tool,
   Components.isabelle_tool,
-  isabelle.find_facts.Find_Facts.isabelle_tool1,
   isabelle.find_facts.Find_Facts.isabelle_tool2,
-  isabelle.find_facts.Find_Facts.isabelle_tool3,
   isabelle.vscode.Component_VSCode.isabelle_tool,
   isabelle.vscode.Component_VSCodium.isabelle_tool1,
   isabelle.vscode.Component_VSCodium.isabelle_tool2)
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/Tools/find_facts	Sun Jan 12 00:05:01 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: run find_facts server
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Tool "$@"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/Tools/find_facts_index	Sun Jan 12 00:05:01 2025 +0100
@@ -0,0 +1,11 @@
+#!/usr/bin/env bash
+#
+# DESCRIPTION: index sessions for find_facts
+
+isabelle scala_build || exit $?
+
+eval "declare -a JAVA_ARGS=($ISABELLE_TOOL_JAVA_OPTIONS)"
+
+classpath "$SOLR_JARS"
+
+exec isabelle java "${JAVA_ARGS[@]}" --enable-native-access=ALL-UNNAMED isabelle.find_facts.Find_Facts_Index_Tool "$@"
--- a/src/Tools/Find_Facts/etc/settings	Sat Jan 11 23:33:55 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Sun Jan 12 00:05:01 2025 +0100
@@ -1,3 +1,5 @@
 # -*- shell-script -*- :mode=shellscript:
 
 FIND_FACTS_HOME="$COMPONENT"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sat Jan 11 23:33:55 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 00:05:01 2025 +0100
@@ -635,9 +635,8 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool1 = Isabelle_Tool("find_facts_index", "index sessions for find_facts",
-    Scala_Project.here,
-    { args =>
+  def main_tool1(args: Array[String]): Unit = {
+    Command_Line.tool {
       var clean = false
       val dirs = new mutable.ListBuffer[Path]
       var options = Options.init()
@@ -661,7 +660,9 @@
       val progress = new Console_Progress()
 
       find_facts_index(options, sessions, dirs = dirs.toList, clean = clean, progress = progress)
-    })
+    }
+  }
+
 
 
   /** index components **/
@@ -919,14 +920,14 @@
 
   /* Isabelle tool wrapper */
 
-  val isabelle_tool3 = Isabelle_Tool("find_facts", "run find_facts server", Scala_Project.here,
-  { args =>
-    var devel = false
-    var options = Options.init()
-    var port = 8080
-    var verbose = false
+  def main_tool3 (args: Array[String]): Unit = {
+    Command_Line.tool {
+      var devel = false
+      var options = Options.init()
+      var port = 8080
+      var verbose = false
 
-    val getopts = Getopts("""
+      val getopts = Getopts("""
 Usage: isabelle find_facts [OPTIONS]
 
   Options are:
@@ -942,11 +943,12 @@
         "p:" -> (arg => port = Value.Int.parse(arg)),
         "v" -> (_ => verbose = true))
 
-    val more_args = getopts(args)
-    if (more_args.nonEmpty) getopts.usage()
+      val more_args = getopts(args)
+      if (more_args.nonEmpty) getopts.usage()
+
+      val progress = new Console_Progress(verbose = verbose)
 
-    val progress = new Console_Progress(verbose = verbose)
-
-    find_facts(options, port, devel = devel, progress = progress)
-  })
+      find_facts(options, port, devel = devel, progress = progress)
+    }
+  }
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Find_Facts/src/find_facts_tools.scala	Sun Jan 12 00:05:01 2025 +0100
@@ -0,0 +1,4 @@
+package isabelle.find_facts
+
+object Find_Facts_Index_Tool { def main(args: Array[String]): Unit = Find_Facts.main_tool1(args) }
+object Find_Facts_Tool { def main(args: Array[String]): Unit = Find_Facts.main_tool3(args) }