# HG changeset patch
# User wenzelm
# Date 1660471307 -7200
# Node ID 2b2c09f4e7b5fde651475a2b1d394b5863537ca5
# Parent  7164f537370f3595ae8351fbb76a55cef5fba86e
proper export theory_names: theory/parents are not necessarily present (amending 4d27b520622a);

diff -r 7164f537370f -r 2b2c09f4e7b5 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 14 11:39:28 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 14 12:01:47 2022 +0200
@@ -23,7 +23,6 @@
   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("/")
@@ -88,8 +87,7 @@
 
   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, name = THEORY_PARENTS)) +
+      Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
       " ORDER BY " + Data.theory_name
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
@@ -363,26 +361,27 @@
 
     private def select[A](
       session: String,
-      select1: Entry_Name => Option[A],
-      select2: Session_Database => List[A]
+      select: Session_Database => List[A],
+      project: Entry_Name => A,
+      sort_key: A => String
     ): List[A] = {
-      def sel(name: String): List[A] =
+      def result(name: String): List[A] =
         if (name == Sessions.DRAFT) {
           (for {
             snapshot <- document_snapshot.iterator
             entry_name <- snapshot.all_exports.keysIterator
-            res <- select1(entry_name).iterator
-          } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
+          } yield project(entry_name)).toSet.toList.sortBy(sort_key)
         }
-        else { session_database(name).map(select2).getOrElse(Nil) }
-      if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
+        else session_database(name).map(select).getOrElse(Nil)
+
+      if (session.nonEmpty) result(session) else session_stack.flatMap(result)
     }
 
     def entry_names(session: String = session_name): List[Entry_Name] =
-      select(session, Some(_), _.entry_names)
+      select(session, _.entry_names, identity, _.compound_name)
 
     def theory_names(session: String = session_name): List[String] =
-      select(session, a => if(a.name == THEORY_PARENTS) Some(a.theory) else None, _.theory_names)
+      select(session, _.theory_names, _.theory, identity)
 
     def get(theory: String, name: String): Option[Entry] =
     {
diff -r 7164f537370f -r 2b2c09f4e7b5 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Aug 14 11:39:28 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Aug 14 12:01:47 2022 +0200
@@ -101,7 +101,7 @@
   }
 
   def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
-    theory_context.get(Export.THEORY_PARENTS)
+    theory_context.get(Export.THEORY_PREFIX + "parents")
       .map(entry => Library.trim_split_lines(entry.uncompressed.text))
 
   def no_theory: Theory =