clarified CLI arg vs. option;
--- a/src/Tools/Find_Facts/src/find_facts.scala Tue Jan 21 17:19:30 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala Tue Jan 21 17:28:09 2025 +0100
@@ -729,12 +729,11 @@
}
def find_facts_index_build(
- options: Options,
+ database: String,
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
val solr = Solr.init(solr_data_dir)
- val database = options.string("find_facts_database_name")
val component = "find_facts-" + database
val component_dir =
@@ -751,27 +750,28 @@
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_build
+ Usage: isabelle find_facts_index_build DATABASE
Options are:
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-D DIR target directory (default ".")
- Build Isabelle component from finalized Find_Facts index with given name.
+ Build Isabelle component from finalized Find_Facts index with given database name.
""",
- "o:" -> (arg => options = options + arg),
"D:" -> (arg => target_dir = Path.explode(arg)))
val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
+ val database =
+ more_args match {
+ case database :: Nil => database
+ case _ => getopts.usage()
+ }
val progress = new Console_Progress()
- find_facts_index_build(options, target_dir = target_dir, progress = progress)
+ find_facts_index_build(database, target_dir = target_dir, progress = progress)
})