--- 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)
}
}