# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737475986 -3600
# Node ID 560c7ff87f748b5cd7bb8b0c499b7c8850f21df0
# Parent  234bac3f2730bf34b22eb422d54ae6b98979fcbe
clarified CLI options: web dir only in $FIND_FACTS_HOME_USER/web;

diff -r 234bac3f2730 -r 560c7ff87f74 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 15:55:30 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Tue Jan 21 17:13:06 2025 +0100
@@ -878,8 +878,8 @@
 
   /* find facts */
 
-  val template_web_dir: Path = Path.explode("$FIND_FACTS_HOME/web")
-  val default_web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
+  val web_sources: Path = Path.explode("$FIND_FACTS_HOME/web")
+  val web_dir: Path = Path.explode("$FIND_FACTS_HOME_USER/web")
 
   val default_port = 8080
 
@@ -887,10 +887,9 @@
     options: Options,
     port: Int = default_port,
     devel: Boolean = false,
-    web_dir: Path = default_web_dir,
     progress: Progress = new Progress
   ): Unit = {
-    Isabelle_System.copy_dir(template_web_dir, web_dir, direct = true)
+    Isabelle_System.copy_dir(web_sources, web_dir, direct = true)
 
     val database = options.string("find_facts_database_name")
     val encode = new Encode(options)
@@ -973,7 +972,6 @@
       var options = Options.init()
       var port = default_port
       var verbose = false
-      var web_dir = default_web_dir
 
       val getopts = Getopts("""
 Usage: isabelle find_facts_server [OPTIONS]
@@ -983,22 +981,20 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p PORT      explicit web server port (default: """ + default_port + """)
     -v           verbose server
-    -w DIR       web directory (default: """ + default_web_dir + """)
 
   Run server for Find_Facts.
 """,
         "d" -> (_ => devel = true),
         "o:" -> (arg => options = options + arg),
         "p:" -> (arg => port = Value.Int.parse(arg)),
-        "v" -> (_ => verbose = true),
-        "w:" -> (arg => web_dir = Path.explode(arg)))
+        "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress(verbose = verbose)
 
-      find_facts(options, port = port, devel = devel, web_dir = web_dir, progress = progress)
+      find_facts(options, port = port, devel = devel, progress = progress)
     }
   }
 }