# HG changeset patch
# User wenzelm
# Date 1736634835 -3600
# Node ID 5589ab62869eaef34c7a94cd2ea22327f4a7bb24
# Parent  f54881ce5cf32341942f79913deaec59cfc184ae
clarified options;

diff -r f54881ce5cf3 -r 5589ab62869e src/Tools/Find_Facts/etc/options
--- a/src/Tools/Find_Facts/etc/options	Sat Jan 11 23:24:32 2025 +0100
+++ b/src/Tools/Find_Facts/etc/options	Sat Jan 11 23:33:55 2025 +0100
@@ -1,9 +1,11 @@
+(* :mode=isabelle-options: *)
+
 section "Find Facts"
 
 option find_facts_database_name : string = "local"
 
-option browser_info_url_library : string = "https://isabelle.in.tum.de/dist/library/"
+option find_facts_url_library : string = "https://isabelle.in.tum.de/dist/library/"
   -- "base url for Isabelle HTML presentation"
 
-option browser_info_url_afp : string = "https://www.isa-afp.org/browser_info/current/"
+option find_facts_url_afp : string = "https://www.isa-afp.org/browser_info/current/"
   -- "base url for AFP HTML presentation"
diff -r f54881ce5cf3 -r 5589ab62869e src/Tools/Find_Facts/src/find_facts.scala
--- a/src/Tools/Find_Facts/src/find_facts.scala	Sat Jan 11 23:24:32 2025 +0100
+++ b/src/Tools/Find_Facts/src/find_facts.scala	Sat Jan 11 23:33:55 2025 +0100
@@ -761,8 +761,8 @@
   case class Result(blocks: Blocks, facets: Facets)
 
   class Encode(options: Options) {
-    val library_base_url = Url(options.string("browser_info_url_library"))
-    val afp_base_url = Url(options.string("browser_info_url_afp"))
+    val library_base_url = Url(options.string("find_facts_url_library"))
+    val afp_base_url = Url(options.string("find_facts_url_afp"))
 
     def url(block: Block): Url = {
       val base_url = if (block.chapter == AFP.chapter) afp_base_url else library_base_url