tuned signature;
authorwenzelm
Sun, 07 Aug 2022 12:37:15 +0200
changeset 75788 0132026e26eb
parent 75787 f9fcf06aa2eb
child 75789 4827096caeb5
tuned signature;
src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sun Aug 07 12:30:09 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sun Aug 07 12:37:15 2022 +0200
@@ -247,8 +247,8 @@
   extends AutoCloseable {
     def close(): Unit = ()
 
-    lazy val theory_names: List[String] = read_theory_names(db, session)
-    lazy val entry_names: List[Entry_Name] = read_entry_names(db, session)
+    lazy private [Export] val theory_names: List[String] = read_theory_names(db, session)
+    lazy private [Export] val entry_names: List[Entry_Name] = read_entry_names(db, session)
   }
 
   def open_database_context(store: Sessions.Store): Database_Context = {