# HG changeset patch
# User wenzelm
# Date 1736713590 -3600
# Node ID 2856d67c8879f89efab3436e1014d2ec4c996c11
# Parent  9f3169b9d2d2b177cbd2f810aa1529ef7728582d
explicit settings FIND_FACTS_WEB and option -w, outside of source (immutable) directory;

diff -r 9f3169b9d2d2 -r 2856d67c8879 src/Tools/Find_Facts/etc/settings
--- a/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:10:32 2025 +0100
+++ b/src/Tools/Find_Facts/etc/settings	Sun Jan 12 21:26:30 2025 +0100
@@ -1,5 +1,6 @@
 # -*- shell-script -*- :mode=shellscript:
 
 FIND_FACTS_HOME="$COMPONENT"
+FIND_FACTS_WEB="$ISABELLE_HOME_USER/find_facts/web"
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$FIND_FACTS_HOME/Tools"
diff -r 9f3169b9d2d2 -r 2856d67c8879 src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 21:10:32 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sun Jan 12 21:26:30 2025 +0100
@@ -843,19 +843,26 @@
 
   /* find facts */
 
+  val template_web_dir: Path = Path.explode("$FIND_FACTS_HOME/web")
+  val default_web_dir: Path = Path.explode("$FIND_FACTS_WEB")
+
   def find_facts(
     options: Options,
     port: Int,
     devel: Boolean = false,
+    web_dir: Path = default_web_dir,
     progress: Progress = new Progress
   ): Unit = {
+    progress.echo("Web directory " + web_dir.expand)
+    Isabelle_System.copy_dir(template_web_dir, web_dir, direct = true)
+
     val database = options.string("find_facts_database_name")
     val encode = new Encode(options)
-    val logo = Bytes.read(Path.explode("$FIND_FACTS_HOME/web/favicon.ico"))
+    val logo = Bytes.read(web_dir + Path.explode("favicon.ico"))
 
     val isabelle_style = HTML.fonts_css("/fonts/" + _) + "\n\n" + File.read(HTML.isabelle_css)
 
-    val project = Elm.Project("Find_Facts", Path.explode("$FIND_FACTS_HOME/web"), head = List(
+    val project = Elm.Project("Find_Facts", web_dir, head = List(
       HTML.style("html,body {width: 100%, height: 100%}"),
       Web_App.More_HTML.icon("data:image/x-icon;base64," + logo.encode_base64.text),
       HTML.style_file("isabelle.css"),
@@ -927,6 +934,7 @@
       var options = Options.init()
       var port = 8080
       var verbose = false
+      var web_dir = default_web_dir
 
       val getopts = Getopts("""
 Usage: isabelle find_facts_server [OPTIONS]
@@ -936,20 +944,22 @@
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p PORT      explicit web server 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))
+        "v" -> (_ => verbose = true),
+        "w:" -> (arg => web_dir = Path.explode(arg)))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       val progress = new Console_Progress(verbose = verbose)
 
-      find_facts(options, port, devel = devel, progress = progress)
+      find_facts(options, port, devel = devel, web_dir = web_dir, progress = progress)
     }
   }
 }