--- 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"
--- 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