src/Pure/Thy/export.scala

   }
 
 
   /* database consumer thread */
 
-  def consumer(db: SQL.Database, cache: XML.Cache): Consumer = new Consumer(db, cache)
-
-  class Consumer private[Export](db: SQL.Database, cache: XML.Cache)
+  def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
+    new Consumer(db, cache, progress)
+
+  class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress)
   {
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(

         consume =
           (args: List[(Entry, Boolean)]) =>
           {
             val results =
               db.transaction {
-                for ((entry, strict) <- args)
+                for ((entry, strict) <- args if !progress.stopped)
                 yield {
                   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 :: _)

 
     def shutdown(close: Boolean = false): List[String] =
     {
       consumer.shutdown()
       if (close) db.close()
-      errors.value.reverse
+      errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
     }
   }
 
 
   /* abstract provider */