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