# HG changeset patch
# User wenzelm
# Date 1525707603 -7200
# Node ID 3795f67716e6ddc08fa3bd781d7f85136612d334
# Parent  c5764b8b2a87ef56d679785dfc46403402fe4efd
tuned;

diff -r c5764b8b2a87 -r 3795f67716e6 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Mon May 07 17:37:03 2018 +0200
+++ b/src/Pure/Thy/export.scala	Mon May 07 17:40:03 2018 +0200
@@ -33,6 +33,9 @@
       stmt.execute_query().iterator(res => res.string(Data.name)).toList)
   }
 
+  def message(msg: String, theory_name: String, name: String): String =
+    msg + " " + quote(name) + " for theory " + quote(theory_name)
+
   sealed case class Entry(
     session_name: String,
     theory_name: String,
@@ -42,9 +45,6 @@
   {
     override def toString: String = theory_name + ":" + name
 
-    def message(msg: String): String =
-      msg + " " + quote(name) + " for theory " + quote(theory_name)
-
     def write(db: SQL.Database)
     {
       val bytes = body.join
@@ -79,7 +79,7 @@
         val body = res.bytes(Data.body)
         Entry(session_name, theory_name, name, compressed, Future.value(body))
       }
-      else error(Entry(session_name, theory_name, name, false, Future.value(Bytes.empty)).message("Bad export"))
+      else error(message("Bad export", theory_name, name))
     })
   }
 
@@ -100,7 +100,8 @@
           entry.body.join
           db.transaction {
             if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
-              export_errors.change(errs => entry.message("Duplicate export") :: errs)
+              val err = message("Duplicate export", entry.theory_name, entry.name)
+              export_errors.change(errs => err :: errs)
             }
             else entry.write(db)
           }