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 {