# HG changeset patch
# User wenzelm
# Date 1631025257 -7200
# Node ID e117e0c29204c4b4f771f928c6d77c93254c5023
# Parent  53e1a14e2ef16f4816a5d6aaf7b34143fabdea53
more reactive interrupt;

diff -r 53e1a14e2ef1 -r e117e0c29204 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Sep 07 15:15:13 2021 +0200
+++ b/src/Pure/Thy/export.scala	Tue Sep 07 16:34:17 2021 +0200
@@ -204,9 +204,10 @@
 
   /* database consumer thread */
 
-  def consumer(db: SQL.Database, cache: XML.Cache): Consumer = new Consumer(db, cache)
+  def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
+    new Consumer(db, cache, progress)
 
-  class Consumer private[Export](db: SQL.Database, cache: XML.Cache)
+  class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress)
   {
     private val errors = Synchronized[List[String]](Nil)
 
@@ -218,7 +219,7 @@
           {
             val results =
               db.transaction {
-                for ((entry, strict) <- args)
+                for ((entry, strict) <- args if !progress.stopped)
                 yield {
                   if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
                     if (strict) {
@@ -240,7 +241,7 @@
     {
       consumer.shutdown()
       if (close) db.close()
-      errors.value.reverse
+      errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
     }
   }
 
diff -r 53e1a14e2ef1 -r e117e0c29204 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Sep 07 15:15:13 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue Sep 07 16:34:17 2021 +0200
@@ -265,7 +265,8 @@
       }
 
       val export_consumer =
-        Export.consumer(store.open_database(session_name, output = true), store.cache)
+        Export.consumer(store.open_database(session_name, output = true), store.cache,
+          progress = progress)
 
       val stdout = new StringBuilder(1000)
       val stderr = new StringBuilder(1000)