diff --git a/src/Tools/jEdit/src/document_dockable.scala b/src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala
+++ b/src/Tools/jEdit/src/document_dockable.scala
@@ -1,381 +1,378 @@
 /*  Title:      Tools/jEdit/src/document_dockable.scala
     Author:     Makarius
 
 Dockable window for document build support.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import scala.swing.{ScrollPane, TextArea, Label, TabbedPane, BorderPanel, Component}
 import scala.swing.event.SelectionChanged
 
 import org.gjt.sp.jedit.{jEdit, View}
 
 
 object Document_Dockable {
   /* state */
 
   object Status extends Enumeration {
     val WAITING = Value("waiting")
     val RUNNING = Value("running")
     val FINISHED = Value("finished")
   }
 
   object State {
     def init(): State = State()
   }
 
   sealed case class State(
     progress: Progress = new Progress,
     process: Future[Unit] = Future.value(()),
     status: Status.Value = Status.FINISHED,
     output_results: Command.Results = Command.Results.empty,
     output_main: XML.Body = Nil,
     output_more: XML.Body = Nil
   ) {
     def run(progress: Progress, process: Future[Unit]): State =
       copy(progress = progress, process = process, status = Status.RUNNING)
 
     def running(results: Command.Results, body: XML.Body): State =
       copy(status = Status.RUNNING, output_results = results, output_main = body)
 
     def finish(output: XML.Body): State =
       copy(process = Future.value(()), status = Status.FINISHED, output_more = output)
 
     def output_body: XML.Body =
       output_main :::
       (if (output_main.nonEmpty && output_more.nonEmpty) Pretty.Separator else Nil) :::
       output_more
 
     def ok: Boolean = !output_body.exists(Protocol.is_error)
   }
 }
 
 class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
   dockable =>
 
   GUI_Thread.require {}
 
 
   /* component state -- owned by GUI thread */
 
   private val current_state = Synchronized(Document_Dockable.State.init())
 
   private val process_indicator = new Process_Indicator
   private val pretty_text_area = new Pretty_Text_Area(view)
   private val message_pane = new TabbedPane
 
   private def show_state(): Unit = GUI_Thread.later {
     val st = current_state.value
 
     pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_body)
 
     st.status match {
       case Document_Dockable.Status.WAITING =>
         process_indicator.update("Waiting for PIDE document content ...", 5)
       case Document_Dockable.Status.RUNNING =>
         process_indicator.update("Running document build process ...", 15)
       case Document_Dockable.Status.FINISHED =>
         process_indicator.update(null, 0)
     }
   }
 
   private def show_page(page: TabbedPane.Page): Unit = GUI_Thread.later {
     message_pane.selection.page = page
   }
 
 
   /* text area with zoom/resize */
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
   private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
   private def handle_resize(): Unit = GUI_Thread.require { pretty_text_area.zoom(zoom) }
 
   private val delay_resize: Delay =
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 
 
   /* progress */
 
   class Log_Progress extends Program_Progress {
     progress =>
 
     override def detect_program(s: String): Option[String] =
       Document_Build.detect_running_script(s)
 
     private val delay: Delay =
       Delay.first(PIDE.session.output_delay) {
         if (!stopped) {
           running_process(progress)
           GUI_Thread.later { show_state() }
         }
       }
 
     override def echo(msg: String): Unit = { super.echo(msg); delay.invoke() }
     override def stop_program(): Unit = { super.stop_program(); delay.invoke() }
   }
 
 
   /* document build process */
 
   private def init_state(): Unit =
     current_state.change { st =>
       st.progress.stop()
       Document_Dockable.State(progress = new Log_Progress)
     }
 
   private def cancel_process(): Unit =
     current_state.change { st => st.process.cancel(); st }
 
   private def await_process(): Unit =
     current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
 
   private def running_process(progress: Log_Progress): Unit = {
     val (results, body) = progress.output()
     current_state.change(_.running(results, body))
   }
 
   private def finish_process(output: XML.Body): Unit =
     current_state.change(_.finish(output))
 
   private def run_process(only_running: Boolean = false)(body: Log_Progress => Unit): Boolean = {
     val started =
       current_state.change_result { st =>
         if (st.process.is_finished) {
           st.progress.stop()
           val progress = new Log_Progress
           val process =
             Future.thread[Unit](name = "Document_Dockable.process") {
               await_process()
               body(progress)
             }
           (true, st.run(progress, process))
         }
         else (false, st)
       }
     show_state()
     started
   }
 
   private def load_document(session: String): Boolean = {
     val options = PIDE.options.value
     run_process() { _ =>
       try {
         val session_background =
           Document_Build.session_background(
             options, session, dirs = JEdit_Sessions.session_dirs)
         PIDE.editor.document_setup(Some(session_background))
 
         finish_process(Nil)
         GUI_Thread.later {
           refresh_theories()
           show_state()
           show_page(input_page)
         }
       }
       catch {
         case exn: Throwable if !Exn.is_interrupt(exn) =>
           finish_process(List(Protocol.error_message(Exn.print(exn))))
           GUI_Thread.later {
             show_state()
             show_page(output_page)
           }
       }
     }
   }
 
   private def document_build(
     session_background: Sessions.Background,
     progress: Log_Progress
   ): Unit = {
-    val store = JEdit_Sessions.sessions_store(PIDE.options.value)
     val document_selection = PIDE.editor.document_selection()
 
     val snapshot = PIDE.session.await_stable_snapshot()
-    val session_context =
-      Export.open_session_context(store, PIDE.resources.session_background,
-        document_snapshot = Some(snapshot))
+    val session_context = JEdit_Sessions.open_session_context(document_snapshot = Some(snapshot))
     try {
       val context =
         Document_Build.context(session_context,
           document_session = Some(session_background.base),
           document_selection = document_selection,
           progress = progress)
 
       val variant = session_background.info.documents.head
 
       Isabelle_System.make_directory(Document_Editor.document_output_dir())
       val doc = context.build_document(variant, verbose = true)
 
       File.write(Document_Editor.document_output().log, doc.log)
       Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
       Document_Editor.view_document()
     }
     finally { session_context.close() }
   }
 
   private def build_document(): Unit = {
     PIDE.editor.document_session() match {
       case Some(session_background) if session_background.info.documents.nonEmpty =>
         run_process(only_running = true) { progress =>
           show_page(output_page)
           val result = Exn.capture { document_build(session_background, progress) }
           val msgs =
             result match {
               case Exn.Res(_) =>
                 List(Protocol.writeln_message("OK"))
               case Exn.Exn(exn: Document_Build.Build_Error) =>
                 exn.log_errors.map(s => Protocol.error_message(YXML.parse_body(s)))
               case Exn.Exn(exn) =>
                 List(Protocol.error_message(YXML.parse_body(Exn.print(exn))))
             }
 
           progress.stop_program()
           running_process(progress)
           finish_process(Pretty.separate(msgs))
 
           show_state()
           show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page)
         }
       case _ =>
     }
   }
 
 
   /* controls */
 
   private val document_session =
     JEdit_Sessions.document_selector(PIDE.options, standalone = true)
 
   private lazy val delay_load: Delay =
     Delay.last(PIDE.session.load_delay, gui = true) {
       for (session <- document_session.selection_value) {
         if (!load_document(session)) delay_load.invoke()
       }
     }
 
   document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() }
 
   private val load_button =
     new GUI.Button("Load") {
       tooltip = "Load document theories"
       override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
     }
 
   private val build_button =
     new GUI.Button("<html><b>Build</b></html>") {
       tooltip = "Build document"
       override def clicked(): Unit = build_document()
     }
 
   private val cancel_button =
     new GUI.Button("Cancel") {
       tooltip = "Cancel build process"
       override def clicked(): Unit = cancel_process()
     }
 
   private val view_button =
     new GUI.Button("View") {
       tooltip = "View document"
       override def clicked(): Unit = Document_Editor.view_document()
     }
 
   private val controls =
     Wrap_Panel(List(document_session, process_indicator.component, load_button,
       build_button, view_button, cancel_button))
 
   add(controls.peer, BorderLayout.NORTH)
 
   override def focusOnDefaultComponent(): Unit = build_button.requestFocus()
 
 
   /* message pane with pages */
 
   private val reset_button =
     new GUI.Button("Reset") {
       tooltip = "Deselect document theories"
       override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
     }
 
   private val purge_button = new GUI.Button("Purge") {
     tooltip = "Remove theories that are no longer required"
     override def clicked(): Unit = PIDE.editor.purge()
   }
 
   private val theories_controls =
     Wrap_Panel(List(reset_button, purge_button))
 
   private val theories = new Theories_Status(view, document = true)
   private val theories_pane = new ScrollPane(theories.gui)
 
   private def refresh_theories(): Unit = {
     val domain = PIDE.editor.document_theories().toSet
     theories.update(domain = Some(domain), trim = true, force = true)
     theories.refresh()
   }
 
   private val input_page =
     new TabbedPane.Page("Input", new BorderPanel {
       layout(theories_controls) = BorderPanel.Position.North
       layout(theories_pane) = BorderPanel.Position.Center
     }, "Selection and status of document theories")
 
   private val output_controls =
     Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
 
   private val output_page =
     new TabbedPane.Page("Output", new BorderPanel {
       layout(output_controls) = BorderPanel.Position.North
       layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
     }, "Results from document build process")
 
   message_pane.pages ++= List(input_page, output_page)
 
   set_content(message_pane)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
           document_session.load()
           handle_resize()
           refresh_theories()
         }
       case changed: Session.Commands_Changed =>
         GUI_Thread.later {
           val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
           if (domain.nonEmpty) theories.update(domain = Some(domain))
         }
     }
 
   override def init(): Unit = {
     PIDE.editor.document_init(dockable)
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     handle_resize()
     delay_load.invoke()
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     delay_resize.revoke()
     PIDE.editor.document_exit(dockable)
   }
 }
diff --git a/src/Tools/jEdit/src/jedit_sessions.scala b/src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala
+++ b/src/Tools/jEdit/src/jedit_sessions.scala
@@ -1,161 +1,172 @@
 /*  Title:      Tools/jEdit/src/jedit_sessions.scala
     Author:     Makarius
 
 Isabelle/jEdit session information, based on implicit process environment
 and explicit options.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 
 object JEdit_Sessions {
   /* session options */
 
   def session_dirs: List[Path] =
     Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")).filterNot(p => p.implode == "-")
 
   def session_no_build: Boolean =
     Isabelle_System.getenv("JEDIT_NO_BUILD") == "true"
 
   def session_options(options: Options): Options = {
     val options1 =
       Isabelle_System.getenv("JEDIT_BUILD_MODE") match {
         case "default" => options
         case mode => options.bool.update("system_heaps", mode == "system")
       }
 
     val options2 =
       Isabelle_System.getenv("JEDIT_ML_PROCESS_POLICY") match {
         case "" => options1
         case s => options1.string.update("ML_process_policy", s)
       }
 
     options2
   }
 
   def sessions_structure(
     options: Options = PIDE.options.value,
     dirs: List[Path] = session_dirs
   ): Sessions.Structure = {
     Sessions.load_structure(session_options(options), dirs = dirs)
   }
 
-  def sessions_store(options: Options): Sessions.Store =
+
+  /* database store */
+
+  def sessions_store(options: Options = PIDE.options.value): Sessions.Store =
     Sessions.store(session_options(options))
 
+  def open_session_context(
+    store: Sessions.Store = sessions_store(),
+    session_background: Sessions.Background = PIDE.resources.session_background,
+    document_snapshot: Option[Document.Snapshot] = None
+  ): Export.Session_Context = {
+    Export.open_session_context(store, session_background, document_snapshot = document_snapshot)
+  }
+
 
   /* raw logic info */
 
   private val jedit_logic_option = "jedit_logic"
 
   def logic_name(options: Options): String =
     Isabelle_System.default_logic(
       Isabelle_System.getenv("JEDIT_LOGIC"),
       options.string(jedit_logic_option))
 
   def logic_ancestor: Option[String] = proper_string(Isabelle_System.getenv("JEDIT_LOGIC_ANCESTOR"))
   def logic_requirements: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_REQUIREMENTS") == "true"
   def logic_include_sessions: List[String] =
     space_explode(':', Isabelle_System.getenv("JEDIT_INCLUDE_SESSIONS"))
 
   def logic_info(options: Options): Option[Sessions.Info] =
     try { sessions_structure(options = options).get(logic_name(options)) }
     catch { case ERROR(_) => None }
 
   def logic_root(options: Options): Position.T =
     if (logic_requirements) logic_info(options).map(_.pos) getOrElse Position.none
     else Position.none
 
 
   /* session selectors */
 
   class Selector(
     val options: Options_Variable,
     val option_name: String,
     standalone: Boolean,
     batches: List[GUI.Selector.Entry[String]]*)
   extends GUI.Selector[String](batches: _*) with JEdit_Options.Entry {
     name = option_name
     tooltip =
       if (standalone) Word.capitalize(options.value.description(option_name))
       else options.value.check_name(option_name).print_default
 
     override val title: String =
       options.value.check_name(option_name).title_jedit
     override def load(): Unit = {
       val value = options.string(option_name)
       for (entry <- find_value(_ == value)) selection.item = entry
     }
     override def save(): Unit =
       for (value <- selection_value) options.string(option_name) = value
 
     override def changed(): Unit = if (standalone) save()
 
     load()
   }
 
   def logic_selector(options: Options_Variable, standalone: Boolean = false): Selector =
     GUI_Thread.require {
       val sessions = sessions_structure(options = options.value)
       val all_sessions = sessions.imports_topological_order
       val main_sessions = all_sessions.filter(name => sessions(name).main_group)
 
       val default_entry =
         GUI.Selector.item_description("", "default (" + logic_name(options.value) + ")")
 
       new Selector(options, jedit_logic_option, standalone,
         default_entry :: main_sessions.map(GUI.Selector.item),
         all_sessions.sorted.map(GUI.Selector.item))
     }
 
   def document_selector(options: Options_Variable, standalone: Boolean = false): Selector =
     GUI_Thread.require {
       val sessions = sessions_structure(options = options.value + "document")
       val all_sessions =
         sessions.build_topological_order.filter(name => sessions(name).documents.nonEmpty).sorted
       val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
 
       new Selector(options, "editor_document_session", standalone,
         doc_sessions.map(GUI.Selector.item),
         all_sessions.map(GUI.Selector.item))
     }
 
 
   /* session build process */
 
   def session_background(options: Options): Sessions.Background =
     Sessions.background(options,
       dirs = JEdit_Sessions.session_dirs,
       include_sessions = logic_include_sessions,
       session = logic_name(options),
       session_ancestor = logic_ancestor,
       session_requirements = logic_requirements)
 
   def session_build(
     options: Options,
     progress: Progress = new Progress,
     no_build: Boolean = false
   ): Int = {
     Build.build(session_options(options),
       selection = Sessions.Selection.session(PIDE.resources.session_base.session_name),
       progress = progress, build_heap = true, no_build = no_build, dirs = session_dirs,
       infos = PIDE.resources.session_background.infos).rc
   }
 
   def session_start(options: Options): Unit = {
     val session = PIDE.session
     val session_background = PIDE.resources.session_background
-    val store = sessions_store(options)
+    val store = sessions_store(options = options)
 
     session.phase_changed += PIDE.plugin.session_phase_changed
 
     Isabelle_Process.start(store, store.options, session, session_background,
       logic = session_background.session_name,
       modes =
         (space_explode(',', store.options.string("jedit_print_mode")) :::
          space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
   }
 }