# HG changeset patch
# User wenzelm
# Date 1692608006 -7200
# Node ID cfdb586adbbd416b4ecc281c532f5b24e41a16d9
# Parent  4ffc1933f5d906ec14f12ea7cd3890e61c7a8d17
tuned;

diff -r 4ffc1933f5d9 -r cfdb586adbbd src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 20 22:24:24 2023 +0200
+++ b/src/Pure/Thy/export.scala	Mon Aug 21 10:53:26 2023 +0200
@@ -272,19 +272,16 @@
                   val buffer = new mutable.ListBuffer[Option[Entry]]
 
                   for ((entry, strict) <- args) {
-                    if (progress.stopped) {
+                    if (progress.stopped || known(entry.entry_name)) {
                       buffer += None
-                    }
-                    else if (known(entry.entry_name)) {
-                      if (strict) {
+                      if (strict && known(entry.entry_name)) {
                         val msg = message("Duplicate export", entry.theory_name, entry.name)
                         errors.change(msg :: _)
                       }
-                      buffer += None
                     }
                     else {
+                      buffer += Some(entry)
                       known += entry.entry_name
-                      buffer += Some(entry)
                     }
                   }