# 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] =