diff --git a/src/Pure/Thy/export.scala b/src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala
+++ b/src/Pure/Thy/export.scala
@@ -1,536 +1,534 @@
 /*  Title:      Pure/Thy/export.scala
     Author:     Makarius
 
 Manage theory exports: compressed blobs.
 */
 
 package isabelle
 
 
 import scala.annotation.tailrec
 import scala.util.matching.Regex
 
 
 object Export {
   /* artefact names */
 
   val DOCUMENT_ID = "PIDE/document_id"
   val FILES = "PIDE/files"
   val MARKUP = "PIDE/markup"
   val MESSAGES = "PIDE/messages"
   val DOCUMENT_PREFIX = "document/"
   val DOCUMENT_LATEX = DOCUMENT_PREFIX + "latex"
   val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
   val THEORY_PREFIX: String = "theory/"
   val PROOFS_PREFIX: String = "proofs/"
 
   def explode_name(s: String): List[String] = space_explode('/', s)
   def implode_name(elems: Iterable[String]): String = elems.mkString("/")
 
 
   /* SQL data model */
 
   object Data {
     val session_name = SQL.Column.string("session_name").make_primary_key
     val theory_name = SQL.Column.string("theory_name").make_primary_key
     val name = SQL.Column.string("name").make_primary_key
     val executable = SQL.Column.bool("executable")
     val compressed = SQL.Column.bool("compressed")
     val body = SQL.Column.bytes("body")
 
     val table =
       SQL.Table("isabelle_exports",
         List(session_name, theory_name, name, executable, compressed, body))
 
     def where_equal(session_name: String, theory_name: String = "", name: String = ""): SQL.Source =
       "WHERE " + Data.session_name.equal(session_name) +
         (if (theory_name == "") "" else " AND " + Data.theory_name.equal(theory_name)) +
         (if (name == "") "" else " AND " + Data.name.equal(name))
   }
 
   def compound_name(a: String, b: String): String =
     if (a.isEmpty) b else a + ":" + b
 
   sealed case class Entry_Name(session: String = "", theory: String = "", name: String = "") {
     val compound_name: String = Export.compound_name(theory, name)
 
     def make_path(prune: Int = 0): Path = {
       val elems = theory :: space_explode('/', name)
       if (elems.length < prune + 1) {
         error("Cannot prune path by " + prune + " element(s): " + Path.make(elems))
       }
       else Path.make(elems.drop(prune))
     }
 
     def readable(db: SQL.Database): Boolean = {
       val select = Data.table.select(List(Data.name), Data.where_equal(session, theory, name))
       db.using_statement(select)(stmt => stmt.execute_query().next())
     }
 
     def read(db: SQL.Database, cache: XML.Cache): Option[Entry] = {
       val select =
         Data.table.select(List(Data.executable, Data.compressed, Data.body),
           Data.where_equal(session, theory, name))
       db.using_statement(select) { stmt =>
         val res = stmt.execute_query()
         if (res.next()) {
           val executable = res.bool(Data.executable)
           val compressed = res.bool(Data.compressed)
           val bytes = res.bytes(Data.body)
           val body = Future.value(compressed, bytes)
           Some(Entry(this, executable, body, cache))
         }
         else None
       }
     }
   }
 
   def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
     val select =
       Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true)
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
   }
 
   def read_entry_names(db: SQL.Database, session_name: String): List[Entry_Name] = {
     val select =
       Data.table.select(List(Data.theory_name, Data.name), Data.where_equal(session_name)) +
       " ORDER BY " + Data.theory_name + ", " + Data.name
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res =>
         Entry_Name(session = session_name,
           theory = res.string(Data.theory_name),
           name = res.string(Data.name))).toList)
   }
 
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
   def empty_entry(theory_name: String, name: String): Entry =
     Entry(Entry_Name(theory = theory_name, name = name),
       false, Future.value(false, Bytes.empty), XML.Cache.none)
 
   sealed case class Entry(
     entry_name: Entry_Name,
     executable: Boolean,
     body: Future[(Boolean, Bytes)],
     cache: XML.Cache
   ) {
     def session_name: String = entry_name.session
     def theory_name: String = entry_name.theory
     def name: String = entry_name.name
     override def toString: String = name
 
     def compound_name: String = entry_name.compound_name
 
     def name_has_prefix(s: String): Boolean = name.startsWith(s)
     val name_elems: List[String] = explode_name(name)
 
     def name_extends(elems: List[String]): Boolean =
       name_elems.startsWith(elems) && name_elems != elems
 
     def text: String = uncompressed.text
 
     def uncompressed: Bytes = {
       val (compressed, bytes) = body.join
       if (compressed) bytes.uncompress(cache = cache.xz) else bytes
     }
 
     def uncompressed_yxml: XML.Body =
       YXML.parse_body(UTF8.decode_permissive(uncompressed), cache = cache)
 
     def write(db: SQL.Database): Unit = {
       val (compressed, bytes) = body.join
       db.using_statement(Data.table.insert()) { stmt =>
         stmt.string(1) = session_name
         stmt.string(2) = theory_name
         stmt.string(3) = name
         stmt.bool(4) = executable
         stmt.bool(5) = compressed
         stmt.bytes(6) = bytes
         stmt.execute()
       }
     }
   }
 
   def make_regex(pattern: String): Regex = {
     @tailrec def make(result: List[String], depth: Int, chs: List[Char]): Regex =
       chs match {
         case '*' :: '*' :: rest => make("[^:]*" :: result, depth, rest)
         case '*' :: rest => make("[^:/]*" :: result, depth, rest)
         case '?' :: rest => make("[^:/]" :: result, depth, rest)
         case '\\' :: c :: rest => make(("\\" + c) :: result, depth, rest)
         case '{' :: rest => make("(" :: result, depth + 1, rest)
         case ',' :: rest if depth > 0 => make("|" :: result, depth, rest)
         case '}' :: rest if depth > 0 => make(")" :: result, depth - 1, rest)
         case c :: rest if ".+()".contains(c) => make(("\\" + c) :: result, depth, rest)
         case c :: rest => make(c.toString :: result, depth, rest)
         case Nil => result.reverse.mkString.r
       }
     make(Nil, 0, pattern.toList)
   }
 
   def make_matcher(pats: List[String]): Entry_Name => Boolean = {
     val regs = pats.map(make_regex)
     (entry_name: Entry_Name) =>
       regs.exists(_.pattern.matcher(entry_name.compound_name).matches)
   }
 
   def make_entry(
     session_name: String,
     args: Protocol.Export.Args,
     bytes: Bytes,
     cache: XML.Cache
   ): Entry = {
     val body =
       if (args.compress) Future.fork(bytes.maybe_compress(cache = cache.xz))
       else Future.value((false, bytes))
     val entry_name = Entry_Name(session = session_name, theory = args.theory_name, name = args.name)
     Entry(entry_name, args.executable, body, cache)
   }
 
 
   /* specific entries */
 
   def read_document_id(read: String => Entry): Option[Long] =
     read(DOCUMENT_ID).text match {
       case Value.Long(id) => Some(id)
       case _ => None
     }
 
   def read_files(read: String => Entry): Option[(String, List[String])] =
     split_lines(read(FILES).text) match {
       case thy_file :: blobs_files => Some((thy_file, blobs_files))
       case Nil => None
     }
 
 
   /* database consumer thread */
 
   def consumer(db: SQL.Database, cache: XML.Cache, progress: Progress = new Progress): Consumer =
     new Consumer(db, cache, progress)
 
   class Consumer private[Export](db: SQL.Database, cache: XML.Cache, progress: Progress) {
     private val errors = Synchronized[List[String]](Nil)
 
     private val consumer =
       Consumer_Thread.fork_bulk[(Entry, Boolean)](name = "export")(
         bulk = { case (entry, _) => entry.body.is_finished },
         consume =
           { (args: List[(Entry, Boolean)]) =>
             val results =
               db.transaction {
                 for ((entry, strict) <- args)
                 yield {
                   if (progress.stopped) {
                     entry.body.cancel()
                     Exn.Res(())
                   }
                   else if (entry.entry_name.readable(db)) {
                     if (strict) {
                       val msg = message("Duplicate export", entry.theory_name, entry.name)
                       errors.change(msg :: _)
                     }
                     Exn.Res(())
                   }
                   else Exn.capture { entry.write(db) }
                 }
               }
             (results, true)
           })
 
     def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = {
       if (!progress.stopped && !body.is_empty) {
         consumer.send(Export.make_entry(session_name, args, body, cache) -> args.strict)
       }
     }
 
     def shutdown(close: Boolean = false): List[String] = {
       consumer.shutdown()
       if (close) db.close()
       errors.value.reverse ::: (if (progress.stopped) List("Export stopped") else Nil)
     }
   }
 
 
   /* abstract provider */
 
   object Provider {
     private def database_provider(
         db: SQL.Database,
         cache: XML.Cache,
         session: String,
         theory: String,
         _theory_names: Synchronized[Option[List[String]]]
     ): Provider = {
       new Provider {
         override def theory_names: List[String] =
           _theory_names.change_result { st =>
             val res = st.getOrElse(read_theory_names(db, session))
             (res, Some(res))
           }
 
         override def apply(export_name: String): Option[Entry] =
           if (theory.isEmpty) None
           else {
             Entry_Name(session = session, theory = theory, name = export_name)
               .read(db, cache)
           }
 
         override def focus(other_theory: String): Provider =
           if (other_theory == theory) this
           else database_provider(db, cache, session, theory, _theory_names)
 
         override def toString: String = db.toString
       }
     }
 
     def database(
       db: SQL.Database,
       cache: XML.Cache,
       session: String,
       theory: String = ""
     ): Provider = database_provider(db, cache, session, theory, Synchronized(None))
 
     def snapshot(
       resources: Resources,
       snapshot: Document.Snapshot
     ): Provider =
       new Provider {
         override def theory_names: List[String] =
           (for {
             (name, _) <- snapshot.version.nodes.iterator
             if name.is_theory && !resources.session_base.loaded_theory(name)
           } yield name.theory).toList
 
         override def apply(export_name: String): Option[Entry] =
           snapshot.exports_map.get(export_name)
 
         override def focus(other_theory: String): Provider =
           if (other_theory == snapshot.node_name.theory) this
           else {
             val node_name =
               snapshot.version.nodes.theory_name(other_theory) getOrElse
                 error("Bad theory " + quote(other_theory))
             Provider.snapshot(resources, snapshot.state.snapshot(node_name))
           }
 
         override def toString: String = snapshot.toString
       }
   }
 
   trait Provider {
     def theory_names: List[String]
 
     def apply(export_name: String): Option[Entry]
 
     def uncompressed_yxml(export_name: String): XML.Body =
       apply(export_name) match {
         case Some(entry) => entry.uncompressed_yxml
         case None => Nil
       }
 
     def focus(other_theory: String): Provider
   }
 
 
   /* context for retrieval */
 
   def context(db_context: Sessions.Database_Context): Context = new Context(db_context)
 
   def open_context(store: Sessions.Store): Context =
     new Context(store.open_database_context()) { override def close(): Unit = db_context.close() }
 
-  def open_context(options: Options): Context = open_context(Sessions.store(options))
-
   class Session_Database private[Export](val session: String, val db: SQL.Database) {
     def close(): Unit = ()
   }
 
   class Context private[Export](val db_context: Sessions.Database_Context) extends AutoCloseable {
     def close(): Unit = ()
 
     def open_session(
       session: String,
       resources: Resources,
       snapshot: Document.Snapshot = Document.Snapshot.init
     ): Session_Context = {
       val session_hierarchy = resources.sessions_structure.build_hierarchy(session)
       db_context.database_server match {
         case Some(db) =>
           val session_database = new Session_Database(session, db)
           new Session_Context(resources, snapshot, db_context.cache, List(session_database))
         case None =>
           val store = db_context.store
           val session_databases = {
             val res = session_hierarchy.map(name => name -> store.try_open_database(name))
             res.collectFirst({ case (name, None) => name }) match {
               case None =>
                 for ((name, Some(db)) <- res)
                 yield {
                   new Session_Database(name, db) { override def close(): Unit = this.db.close() }
                 }
               case Some(bad) =>
                 for ((_, Some(db)) <- res) db.close()
                 store.bad_database(bad)
             }
           }
           new Session_Context(resources, snapshot, db_context.cache, session_databases) {
             override def close(): Unit = db_hierarchy.foreach(_.close())
           }
       }
     }
 
     override def toString: String = db_context.toString
   }
 
   class Session_Context private[Export](
     val resources: Resources,
     val snapshot: Document.Snapshot,
     val cache: Term.Cache,
     val db_hierarchy: List[Session_Database]
   ) extends AutoCloseable {
     session_context =>
 
     def close(): Unit = ()
 
     def get(theory: String, name: String): Option[Entry] =
       snapshot.exports_map.get(name) orElse
         db_hierarchy.view.map(session_db =>
           Export.Entry_Name(session = session_db.session, theory = theory, name = name)
             .read(session_db.db, cache))
           .collectFirst({ case Some(entry) => entry })
 
     def apply(theory: String, name: String, permissive: Boolean = false): Entry =
       get(theory, name) match {
         case None if permissive => empty_entry(theory, name)
         case None => error("Missing export entry " + quote(compound_name(theory, name)))
         case Some(entry) => entry
       }
 
     def theory(theory: String): Theory_Context =
       new Theory_Context(session_context, theory)
 
     override def toString: String =
       "Export.Session_Context(" + commas_quote(db_hierarchy.map(_.session)) + ")"
   }
 
   class Theory_Context private[Export](session_context: Session_Context, theory: String) {
     def get(name: String): Option[Entry] = session_context.get(theory, name)
     def apply(name: String, permissive: Boolean = false): Entry =
       session_context.apply(theory, name, permissive = permissive)
 
     override def toString: String = "Export.Theory_Context(" + quote(theory) + ")"
   }
 
 
   /* export to file-system */
 
   def export_files(
     store: Sessions.Store,
     session_name: String,
     export_dir: Path,
     progress: Progress = new Progress,
     export_prune: Int = 0,
     export_list: Boolean = false,
     export_patterns: List[String] = Nil
   ): Unit = {
     using(store.open_database(session_name)) { db =>
       val entry_names = read_entry_names(db, session_name)
 
       // list
       if (export_list) {
         for (entry_name <- entry_names) progress.echo(entry_name.compound_name)
       }
 
       // export
       if (export_patterns.nonEmpty) {
         val matcher = make_matcher(export_patterns)
         for {
           entry_name <- entry_names if matcher(entry_name)
           entry <- entry_name.read(db, store.cache)
         } {
           val path = export_dir + entry_name.make_path(prune = export_prune)
           progress.echo("export " + path + (if (entry.executable) " (executable)" else ""))
           Isabelle_System.make_directory(path.dir)
           val bytes = entry.uncompressed
           if (!path.is_file || Bytes.read(path) != bytes) Bytes.write(path, bytes)
           File.set_executable(path, entry.executable)
         }
       }
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val default_export_dir: Path = Path.explode("export")
 
   val isabelle_tool =
     Isabelle_Tool("export", "retrieve theory exports", Scala_Project.here,
       { args =>
         /* arguments */
 
         var export_dir = default_export_dir
         var dirs: List[Path] = Nil
         var export_list = false
         var no_build = false
         var options = Options.init()
         var export_prune = 0
         var export_patterns: List[String] = Nil
 
         val getopts = Getopts("""
 Usage: isabelle export [OPTIONS] SESSION
 
   Options are:
     -O DIR       output directory for exported files (default: """ + default_export_dir + """)
     -d DIR       include session directory
     -l           list exports
     -n           no build of session
     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
     -p NUM       prune path of exported files by NUM elements
     -x PATTERN   extract files matching pattern (e.g. "*:**" for all)
 
   List or export theory exports for SESSION: named blobs produced by
   isabelle build. Option -l or -x is required; option -x may be repeated.
 
   The PATTERN language resembles glob patterns in the shell, with ? and *
   (both excluding ":" and "/"), ** (excluding ":"), and [abc] or [^abc],
   and variants {pattern1,pattern2,pattern3}.
 """,
           "O:" -> (arg => export_dir = Path.explode(arg)),
           "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
           "l" -> (_ => export_list = true),
           "n" -> (_ => no_build = true),
           "o:" -> (arg => options = options + arg),
           "p:" -> (arg => export_prune = Value.Int.parse(arg)),
           "x:" -> (arg => export_patterns ::= arg))
 
         val more_args = getopts(args)
         val session_name =
           more_args match {
             case List(session_name) if export_list || export_patterns.nonEmpty => session_name
             case _ => getopts.usage()
           }
 
         val progress = new Console_Progress()
 
 
         /* build */
 
         if (!no_build) {
           val rc =
             progress.interrupt_handler {
               Build.build_logic(options, session_name, progress = progress, dirs = dirs)
             }
           if (rc != Process_Result.RC.ok) sys.exit(rc)
         }
 
 
         /* export files */
 
         val store = Sessions.store(options)
         export_files(store, session_name, export_dir, progress = progress, export_prune = export_prune,
           export_list = export_list, export_patterns = export_patterns)
       })
 }