# HG changeset patch
# User wenzelm
# Date 1659808429 -7200
# Node ID d31193963e2df4aa44fc5f4c672d91241bcd40b3
# Parent  b33b19deca3a9a0930a9b54e7d5039aa57d425fa
tuned;

diff -r b33b19deca3a -r d31193963e2d src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 06 19:37:31 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 06 19:53:49 2022 +0200
@@ -368,16 +368,16 @@
 
     def get(theory: String, name: String): Option[Entry] =
     {
-      def snapshot_entry =
+      def snapshot_entry: Option[Entry] =
         for {
           snapshot <- document_snapshot
           entry_name = Entry_Name(session = Sessions.DRAFT, theory = theory, name = name)
           entry <- snapshot.all_exports.get(entry_name)
         } yield entry
-      def db_entry =
-        db_hierarchy.view.map(session_db =>
-          Export.Entry_Name(session = session_db.session, theory = theory, name = name)
-            .read(session_db.db, cache))
+      def db_entry: Option[Entry] =
+        db_hierarchy.view.map(database =>
+          Export.Entry_Name(session = database.session, theory = theory, name = name)
+            .read(database.db, cache))
           .collectFirst({ case Some(entry) => entry })
 
       snapshot_entry orElse db_entry