--- a/src/Pure/Thy/export.scala Sun Nov 03 16:20:05 2019 +0100
+++ b/src/Pure/Thy/export.scala Sun Nov 03 18:53:48 2019 +0100
@@ -221,6 +221,14 @@
object Provider
{
+ def none: Provider =
+ new Provider {
+ def apply(export_name: String): Option[Entry] = None
+ def focus(other_theory: String): Provider = this
+
+ override def toString: String = "none"
+ }
+
def database(db: SQL.Database, session_name: String, theory_name: String): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =