# HG changeset patch
# User wenzelm
# Date 1631026468 -7200
# Node ID bda7a7b3bd41e9c0d29c355bd74b149d9b38f933
# Parent  0ba3952f409a3c7f4bc5094b3ad29e60a5603c4b
more reactive interrupt;

diff -r 0ba3952f409a -r bda7a7b3bd41 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Sep 07 16:46:18 2021 +0200
+++ b/src/Pure/Thy/export.scala	Tue Sep 07 16:54:28 2021 +0200
@@ -221,7 +221,10 @@
               db.transaction {
                 for ((entry, strict) <- args)
                 yield {
-                  if (progress.stopped) Exn.Res(())
+                  if (progress.stopped) {
+                    entry.body.cancel()
+                    Exn.Res(())
+                  }
                   else if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
                     if (strict) {
                       val msg = message("Duplicate export", entry.theory_name, entry.name)
@@ -236,7 +239,11 @@
           })
 
     def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit =
-      consumer.send(make_entry(session_name, args, body, cache) -> args.strict)
+    {
+      if (!progress.stopped) {
+        consumer.send(make_entry(session_name, args, body, cache) -> args.strict)
+      }
+    }
 
     def shutdown(close: Boolean = false): List[String] =
     {