--- 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) }