# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737476889 -3600
# Node ID dffa88c87a084c7d5fc6b4c62bab1190d175d71b
# Parent  78b8b776fd1f88f9b33fddab8bd8360fee56717d
clarified CLI arg vs. option;

diff -r 78b8b776fd1f -r dffa88c87a08 src/Tools/Find_Facts/src/find_facts.scala
--- 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)
     })