# HG changeset patch
# User wenzelm
# Date 1572803628 -3600
# Node ID 58022ee70b3576163b700e4cf10f77663355d6fa
# Parent  bfa1017b4553059bbab54433d1ac937615c44364
more operations;

diff -r bfa1017b4553 -r 58022ee70b35 src/Pure/Thy/export.scala
--- 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] =