# HG changeset patch
# User wenzelm
# Date 1525786912 -7200
# Node ID 23c6ae3dd3a046a8766bbe1c33473f6a98f57d7f
# Parent  ce7f35406f37f0885f12e456f5198717b1048091
more efficient query;

diff -r ce7f35406f37 -r 23c6ae3dd3a0 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue May 08 11:47:41 2018 +0200
+++ b/src/Pure/Thy/export.scala	Tue May 08 15:41:52 2018 +0200
@@ -33,6 +33,14 @@
       stmt.execute_query().iterator(res => res.string(Data.name)).toList)
   }
 
+  def read_name(db: SQL.Database, session_name: String, theory_name: String, name: String): Boolean =
+  {
+    val select =
+      Data.table.select(List(Data.name),
+        Data.where_equal(session_name, theory_name) + " AND " + Data.name.equal(name))
+    db.using_statement(select)(stmt => stmt.execute_query().next())
+  }
+
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
@@ -99,7 +107,7 @@
         {
           entry.body.join
           db.transaction {
-            if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
+            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)
             }