# HG changeset patch
# User wenzelm
# Date 1527334588 -7200
# Node ID d20770229f9964907a0fc0f387c73af82083dd85
# Parent  2ae74a278c10ce629e2baa5c09855bdc7d2e5022
tuned signature;

diff -r 2ae74a278c10 -r d20770229f99 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat May 26 13:34:44 2018 +0200
+++ b/src/Pure/Thy/export.scala	Sat May 26 13:36:28 2018 +0200
@@ -187,6 +187,47 @@
   }
 
 
+  /* export to file-system */
+
+  def export_files(
+    store: Sessions.Store,
+    session_name: String,
+    export_dir: Path,
+    progress: Progress = No_Progress,
+    export_list: Boolean = false,
+    export_pattern: String = "")
+  {
+    using(store.open_database(session_name))(db =>
+    {
+      db.transaction {
+        val export_names = read_theory_exports(db, session_name)
+
+        // list
+        if (export_list) {
+          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
+            sorted.foreach(Output.writeln(_, stdout = true))
+        }
+
+        // export
+        if (export_pattern != "") {
+          val xz_cache = XZ.make_cache()
+
+          val matcher = make_matcher(export_pattern)
+          for {
+            (theory_name, name) <- export_names if matcher(theory_name, name)
+            entry <- read_entry(db, session_name, theory_name, name)
+          } {
+            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
+            progress.echo("exporting " + path)
+            Isabelle_System.mkdirs(path.dir)
+            Bytes.write(path, entry.uncompressed(cache = xz_cache))
+          }
+        }
+      }
+    })
+  }
+
+
   /* Isabelle tool wrapper */
 
   val default_export_dir = Path.explode("export")
@@ -256,37 +297,10 @@
     }
 
 
-    /* database */
+    /* export files */
 
     val store = Sessions.store(options, system_mode)
-
-    using(store.open_database(session_name))(db =>
-    {
-      db.transaction {
-        val export_names = read_theory_exports(db, session_name)
-
-        // list
-        if (export_list) {
-          (for ((theory_name, name) <- export_names) yield compound_name(theory_name, name)).
-            sorted.foreach(Output.writeln(_, stdout = true))
-        }
-
-        // export
-        if (export_pattern != "") {
-          val xz_cache = XZ.make_cache()
-
-          val matcher = make_matcher(export_pattern)
-          for {
-            (theory_name, name) <- export_names if matcher(theory_name, name)
-            entry <- read_entry(db, session_name, theory_name, name)
-          } {
-            val path = export_dir + Path.basic(theory_name) + Path.explode(name)
-            progress.echo("exporting " + path)
-            Isabelle_System.mkdirs(path.dir)
-            Bytes.write(path, entry.uncompressed(cache = xz_cache))
-          }
-        }
-      }
-    })
+    export_files(store, session_name, export_dir, progress = progress,
+      export_list = export_list, export_pattern = export_pattern)
   })
 }