# HG changeset patch
# User wenzelm
# Date 1739388093 -3600
# Node ID a42414afe05fea884a7e47e87ffef2f5e95dd514
# Parent  2eb2aa0375fb8b5893b8b7866f35eea6c238fa1f
more operations;

diff -r 2eb2aa0375fb -r a42414afe05f src/Pure/General/file_store.scala
--- 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 */