# HG changeset patch
# User wenzelm
# Date 1574267164 -3600
# Node ID 2f782d5f5d5a200a7aa2daa0acd2756907c7154e
# Parent  d6b9dead8c8d507141ab0368bff6ea8805b13b56
improved performance of session exports via bulk transactions;

diff -r d6b9dead8c8d -r 2f782d5f5d5a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Wed Nov 20 16:56:03 2019 +0100
+++ b/src/Pure/Thy/export.scala	Wed Nov 20 17:26:04 2019 +0100
@@ -191,21 +191,27 @@
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
-      Consumer_Thread.fork(name = "export")(consume = (arg: (Entry, Boolean)) =>
-        {
-          val (entry, strict) = arg
-          entry.body.join
-          db.transaction {
-            if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
-              if (strict) {
-                val msg = message("Duplicate export", entry.theory_name, entry.name)
-                errors.change(msg :: _)
+      Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
+        bulk = { case (entry, _) => entry.body.is_finished },
+        consume =
+          (args: List[(Entry, Boolean)]) =>
+          {
+            val results =
+              db.transaction {
+                for ((entry, strict) <- args)
+                yield {
+                  if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
+                    if (strict) {
+                      val msg = message("Duplicate export", entry.theory_name, entry.name)
+                      errors.change(msg :: _)
+                    }
+                    Exn.Res(())
+                  }
+                  else Exn.capture { entry.write(db) }
+                }
               }
-            }
-            else entry.write(db)
-          }
-          true
-        })
+            (results, true)
+          })
 
     def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit =
       consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict)