# HG changeset patch
# User wenzelm
# Date 1659712597 -7200
# Node ID 87f9748b214ac9cc1f0ffd7c8748b9d853226bb8
# Parent  d795d8b5956314e8121a714a4f00ef9e57a3812c
clarified signature: persistent theory_names in lexical order;

diff -r d795d8b59563 -r 87f9748b214a src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Fri Aug 05 16:50:04 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 05 17:16:37 2022 +0200
@@ -87,7 +87,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), distinct = true) +
+      " ORDER BY " + Data.theory_name
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
   }
@@ -343,6 +344,8 @@
 
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
+
+    lazy val theory_names: List[String] = read_theory_names(db, session)
   }
 
   class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
@@ -406,6 +409,9 @@
         case Some(entry) => entry
       }
 
+    def theory_names(session: String): List[String] =
+      db_hierarchy.find(_.session == session).map(_.theory_names).getOrElse(Nil)
+
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)