clarified signature: persistent theory_names in lexical order;
authorwenzelm
Fri, 05 Aug 2022 17:16:37 +0200
changeset 75767 87f9748b214a
parent 75766 d795d8b59563
child 75768 be79948f7f23
clarified signature: persistent theory_names in lexical order;
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)