# HG changeset patch
# User wenzelm
# Date 1739398628 -3600
# Node ID 3312ca0f3915937660ede076ac62d02fbfe5be1b
# Parent  a42414afe05fea884a7e47e87ffef2f5e95dd514
support for browser_info.db --- requires approx. 10s to compress 1.2GB to 152MB;

diff -r a42414afe05f -r 3312ca0f3915 etc/settings
--- a/etc/settings	Wed Feb 12 20:21:33 2025 +0100
+++ b/etc/settings	Wed Feb 12 23:17:08 2025 +0100
@@ -101,6 +101,7 @@
 # HTML browser info.
 ISABELLE_BROWSER_INFO="$ISABELLE_HOME_USER/browser_info"
 ISABELLE_BROWSER_INFO_SYSTEM="$ISABELLE_HOME/browser_info"
+ISABELLE_BROWSER_INFO_LIBRARY="$ISABELLE_HOME/lib/browser_info.db"
 
 # Site settings check -- just to make it a little bit harder to copy this file verbatim!
 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \
diff -r a42414afe05f -r 3312ca0f3915 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Feb 12 20:21:33 2025 +0100
+++ b/src/Pure/Admin/build_release.scala	Wed Feb 12 23:17:08 2025 +0100
@@ -478,12 +478,12 @@
 
       make_news(other_isabelle)
 
-      other_isabelle_purge("browser_info")
-
       if (build_library || include_library || include_find_facts) {
         progress.echo("Presenting library ...")
         require(Platform.is_unix, "Linux or macOS platform required")
 
+        other_isabelle_purge("browser_info")
+
         val opt_dirs = "-d '~~/src/Benchmarks' "
         other_isabelle.bash("bin/isabelle build -f -j " + parallel_jobs +
           " -o browser_info -o document=pdf -o document_variants=document:outline=/proof,/ML" +
@@ -520,11 +520,16 @@
             " " + Bash.string(context.dist_name + "/browser_info"))
         }
 
-        if (!include_library) other_isabelle_purge("browser_info")
+        if (include_library) {
+          Browser_Info.make_database(
+            other_isabelle.expand_path(Browser_Info.default_database),
+            other_isabelle.expand_path(Browser_Info.default_dir))
+        }
       }
 
       other_isabelle_purge("Admin")
       other_isabelle_purge("heaps")
+      other_isabelle_purge("browser_info")
 
       other_isabelle.cleanup()
 
diff -r a42414afe05f -r 3312ca0f3915 src/Pure/Build/browser_info.scala
--- a/src/Pure/Build/browser_info.scala	Wed Feb 12 20:21:33 2025 +0100
+++ b/src/Pure/Build/browser_info.scala	Wed Feb 12 23:17:08 2025 +0100
@@ -12,6 +12,17 @@
 
 
 object Browser_Info {
+  /* SQLite database with compressed entries */
+
+  val default_database: Path = Path.explode("$ISABELLE_BROWSER_INFO_LIBRARY")
+  val default_dir: Path = Path.explode("$ISABELLE_BROWSER_INFO")
+
+  def make_database(database: Path = default_database, dir: Path = default_dir): Unit =
+    File_Store.make_database(database, dir,
+      compress_options = Compress.Options_Zstd(level = 8),
+      compress_cache = Compress.Cache.make())
+
+
   /* browser_info store configuration */
 
   object Config {