# HG changeset patch
# User wenzelm
# Date 1536332638 -7200
# Node ID feed46aa19698a786a19839278aabc8a9f10c325
# Parent  59d2eab3f8b98900f4ae587e006820c114742190
tuned;

diff -r 59d2eab3f8b9 -r feed46aa1969 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Sep 07 14:07:34 2018 +0200
+++ b/src/Pure/Thy/export.scala	Fri Sep 07 17:03:58 2018 +0200
@@ -167,7 +167,7 @@
 
   class Consumer private[Export](db: SQL.Database, cache: XZ.Cache)
   {
-    private val export_errors = Synchronized[List[String]](Nil)
+    private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
       Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
@@ -175,8 +175,8 @@
           entry.body.join
           db.transaction {
             if (read_name(db, entry.session_name, entry.theory_name, entry.name)) {
-              val err = message("Duplicate export", entry.theory_name, entry.name)
-              export_errors.change(errs => err :: errs)
+              val msg = message("Duplicate export", entry.theory_name, entry.name)
+              errors.change(msg :: _)
             }
             else entry.write(db)
           }
@@ -190,7 +190,7 @@
     {
       consumer.shutdown()
       if (close) db.close()
-      export_errors.value.reverse
+      errors.value.reverse
     }
   }