# HG changeset patch # User wenzelm # Date 1736636701 -3600 # Node ID c405ad565d700624f6943c91eacf719402b54dca # Parent 5589ab62869eaef34c7a94cd2ea22327f4a7bb24 tool wrappers with specific java options, notably classpath "$SOLR_JARS"; diff -r 5589ab62869e -r c405ad565d70 etc/build.props --- 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 \ diff -r 5589ab62869e -r c405ad565d70 src/Pure/System/isabelle_tool.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) diff -r 5589ab62869e -r c405ad565d70 src/Tools/Find_Facts/Tools/find_facts --- /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 "$@" diff -r 5589ab62869e -r c405ad565d70 src/Tools/Find_Facts/Tools/find_facts_index --- /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 "$@" diff -r 5589ab62869e -r c405ad565d70 src/Tools/Find_Facts/etc/settings --- 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" diff -r 5589ab62869e -r c405ad565d70 src/Tools/Find_Facts/src/find_facts.scala --- 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) + } + } } diff -r 5589ab62869e -r c405ad565d70 src/Tools/Find_Facts/src/find_facts_tools.scala --- /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) }