# HG changeset patch
# User wenzelm
# Date 1631025978 -7200
# Node ID 0ba3952f409a3c7f4bc5094b3ad29e60a5603c4b
# Parent  e117e0c29204c4b4f771f928c6d77c93254c5023
more robust: retain length of results;

diff -r e117e0c29204 -r 0ba3952f409a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Sep 07 16:34:17 2021 +0200
+++ b/src/Pure/Thy/export.scala	Tue Sep 07 16:46:18 2021 +0200
@@ -219,9 +219,10 @@
           {
             val results =
               db.transaction {
-                for ((entry, strict) <- args if !progress.stopped)
+                for ((entry, strict) <- args)
                 yield {
-                  if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
+                  if (progress.stopped) 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)
                       errors.change(msg :: _)