# HG changeset patch
# User wenzelm
# Date 1660495120 -7200
# Node ID b0215440311d3a5aea6108e6b634ca299ea5a4c0
# Parent  86d60f4a10a76c992881d85e4891619fce1d5f46# Parent  186654cd2840bf7052bf8205f690bdcb21df9fea
merged

diff -r 86d60f4a10a7 -r b0215440311d src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export.scala	Sun Aug 14 18:38:40 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 86d60f4a10a7 -r b0215440311d src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export_theory.ML	Sun Aug 14 18:38:40 2022 +0200
@@ -156,7 +156,7 @@
     val parents = Theory.parents_of thy;
     val _ =
       Export.export thy \<^path_binding>\<open>theory/parents\<close>
-        (XML.Encode.string (terminate_lines (map Context.theory_long_name parents)));
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents) ^ "\n"));
 
 
     (* spec rules *)
diff -r 86d60f4a10a7 -r b0215440311d src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sun Aug 14 18:38:40 2022 +0200
@@ -26,10 +26,11 @@
 
   def read_session(
     session_context: Export.Session_Context,
+    session_stack: Boolean = false,
     progress: Progress = new Progress
   ): Session = {
     val thys =
-      for (theory <- session_context.theory_names()) yield {
+      for (theory <- theory_names(session_context, session_stack = session_stack)) yield {
         progress.echo("Reading theory " + theory)
         read_theory(session_context.theory(theory))
       }
@@ -101,9 +102,20 @@
   }
 
   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 theory_names(
+    session_context: Export.Session_Context,
+    session_stack: Boolean = false
+  ): List[String] = {
+    val session = if (session_stack) "" else session_context.session_name
+    for {
+      theory <- session_context.theory_names(session = session)
+      if read_theory_parents(session_context.theory(theory)).isDefined
+    } yield theory
+  }
+
   def no_theory: Theory =
     Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
 
diff -r 86d60f4a10a7 -r b0215440311d src/Pure/library.ML
--- a/src/Pure/library.ML	Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/library.ML	Sun Aug 14 18:38:40 2022 +0200
@@ -145,7 +145,6 @@
   val commas: string list -> string
   val commas_quote: string list -> string
   val cat_lines: string list -> string
-  val terminate_lines: string list -> string
   val space_explode: string -> string -> string list
   val split_lines: string -> string list
   val plain_words: string -> string
@@ -749,8 +748,6 @@
 
 val cat_lines = space_implode "\n";
 
-fun terminate_lines lines = cat_lines lines ^ "\n";
-
 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
 fun space_explode _ "" = []
   | space_explode sep s = String.fields (fn c => str c = sep) s;
diff -r 86d60f4a10a7 -r b0215440311d src/Pure/library.scala
--- a/src/Pure/library.scala	Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/library.scala	Sun Aug 14 18:38:40 2022 +0200
@@ -94,8 +94,10 @@
 
   /* lines */
 
-  def terminate_lines(lines: IterableOnce[String]): String =
-    lines.iterator.mkString("", "\n", "\n")
+  def terminate_lines(lines: IterableOnce[String]): String = {
+    val it = lines.iterator
+    if (it.isEmpty) "" else it.mkString("", "\n", "\n")
+  }
 
   def cat_lines(lines: IterableOnce[String]): String =
     lines.iterator.mkString("\n")