# HG changeset patch
# User wenzelm
# Date 1659448197 -7200
# Node ID 5934209c49072d3dfa3f6daef368753bd017222c
# Parent  7671f9fc66d74c4c9c9c6e20d918c4a9016a3f68
clarified signature: more robust;

diff -r 7671f9fc66d7 -r 5934209c4907 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Aug 02 12:57:04 2022 +0200
+++ b/src/Pure/Thy/export.scala	Tue Aug 02 15:49:57 2022 +0200
@@ -285,8 +285,11 @@
     ) : Provider = {
       new Provider {
         def apply(export_name: String): Option[Entry] =
-          Entry_Name(session = session_name, theory = theory_name, name = export_name)
-            .read(db, cache)
+          if (theory_name.isEmpty) None
+          else {
+            Entry_Name(session = session_name, theory = theory_name, name = export_name)
+              .read(db, cache)
+          }
 
         def focus(other_theory: String): Provider =
           if (other_theory == theory_name) this