# HG changeset patch
# User wenzelm
# Date 1659718958 -7200
# Node ID 4d27b520622ad6c6d9a0ace2a5e3cfb8f39d9cc1
# Parent  be79948f7f23c8b851554956cefc8ab4ba802665
clarified database query: refer to semantic theories;

diff -r be79948f7f23 -r 4d27b520622a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 18:45:49 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 19:02:38 2022 +0200
@@ -23,6 +23,7 @@
   val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"
+  val THEORY_PARENTS: String = THEORY_PREFIX + "parents"
 
   def explode_name(s: String): List[String] = space_explode('/', s)
   def implode_name(elems: Iterable[String]): String = elems.mkString("/")
@@ -87,7 +88,8 @@
 
   def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
     val select =
-      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
+      Data.table.select(List(Data.theory_name),
+        Data.where_equal(session_name, name = THEORY_PARENTS)) +
       " ORDER BY " + Data.theory_name
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
diff -r be79948f7f23 -r 4d27b520622a src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Aug 05 18:45:49 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Aug 05 19:02:38 2022 +0200
@@ -108,7 +108,7 @@
   }
 
   def read_theory_parents(provider: Export.Provider, theory_name: String): Option[List[String]] =
-    provider.focus(theory_name)(Export.THEORY_PREFIX + "parents")
+    provider.focus(theory_name)(Export.THEORY_PARENTS)
       .map(entry => Library.trim_split_lines(entry.uncompressed.text))
 
   def no_theory: Theory =