more robust: retain length of results;

--- 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 :: _)