--- a/src/Pure/General/file_store.scala Wed Feb 12 20:18:21 2025 +0100
+++ b/src/Pure/General/file_store.scala Wed Feb 12 20:21:33 2025 +0100
@@ -49,6 +49,23 @@
}
else None
+ def database_extract(database: Path, dir: Path,
+ compress_cache: Compress.Cache = Compress.Cache.none
+ ): Unit = {
+ if (database.is_file) {
+ using(SQLite.open_database(database)) { db =>
+ private_data.transaction_lock(db) {
+ if (private_data.tables_ok(db)) {
+ for {
+ name <- private_data.read_names(db)
+ entry <- private_data.read_entry(db, name)
+ } entry.write_file(dir, compress_cache = compress_cache)
+ }
+ }
+ }
+ }
+ }
+
/* entry */