actually build document;
clarified signature;

--- a/src/Pure/PIDE/document_editor.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -32,10 +32,9 @@
 
     override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
 
-    def load(): Unit = GUI_Thread.require {
-      val path = document_output().log
-      val text = if (path.is_file) File.read(path) else ""
-      GUI_Thread.later { delay.revoke(); update(text) }
+    def finish(text: String): Unit = GUI_Thread.require {
+      delay.revoke()
+      update(text)
     }
 
     GUI_Thread.later { update() }

--- a/src/Pure/PIDE/editor.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -40,6 +40,7 @@
   def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name)
 
   def document_theories(): List[Document.Node.Name] = document_state().active_document_theories
+  def document_selection(): Set[Document.Node.Name] = document_state().selection
 
   def document_setup(background: Option[Sessions.Background]): Unit =
     document_state_change(_.copy(session_background = background))

--- a/src/Pure/Thy/document_build.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -135,12 +135,14 @@
   def context(
     session_context: Export.Session_Context,
     document_session: Option[Sessions.Base] = None,
+    document_selection: Document.Node.Name => Boolean = _ => true,
     progress: Progress = new Progress
-  ): Context = new Context(session_context, document_session, progress)
+  ): Context = new Context(session_context, document_session, document_selection, progress)
 
   final class Context private[Document_Build](
     val session_context: Export.Session_Context,
     document_session: Option[Sessions.Base],
+    document_selection: Document.Node.Name => Boolean,
     val progress: Progress
   ) {
     context =>
@@ -187,8 +189,12 @@
       for (name <- all_document_theories)
       yield {
         val path = Path.basic(tex_name(name))
-        val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
-        val content = YXML.parse_body(entry.text)
+        val content =
+          if (document_selection(name)) {
+            val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+            YXML.parse_body(entry.text)
+          }
+          else Nil
         File.content(path, content)
       }
 

--- a/src/Pure/Thy/sessions.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -112,6 +112,7 @@
     infos: List[Info] = Nil
   ) {
     def session_name: String = base.session_name
+    def info: Info = sessions_structure(session_name)
 
     def check_errors: Background =
       if (errors.isEmpty) this

--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Dec 21 14:14:02 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Dec 21 15:34:33 2022 +0100
@@ -176,32 +176,57 @@
     }
   }
 
-  private def build_document(): Unit = {
-    run_process { progress =>
-      show_page(theories_page)
-      Time.seconds(2.0).sleep()
+  private def document_build(
+    session_background: Sessions.Background,
+    progress: Document_Editor.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, session_background,
+        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)
+
+      // log
+      File.write(Document_Editor.document_output().log, doc.log)
+      GUI_Thread.later { progress.finish(doc.log) }
 
-      show_page(log_page)
-      val res =
-        Exn.capture {
-          progress.echo("Start " + Date.now())
-          for (i <- 1 to 200) {
-            progress.echo("message " + i)
-            Time.seconds(0.1).sleep()
-          }
-          progress.echo("Stop " + Date.now())
+      // pdf
+      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 { progress =>
+          show_page(log_page)
+          val res = Exn.capture { document_build(session_background, progress) }
+          val msg =
+            res match {
+              case Exn.Res(_) => Protocol.writeln_message("OK")
+              case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
+            }
+
+          finish_process(List(msg))
+
+          show_state()
+          show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
         }
-      val msg =
-        res match {
-          case Exn.Res(_) => Protocol.writeln_message("OK")
-          case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
-        }
-      finish_process(List(msg))
-
-      show_state()
-
-      show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
-      GUI_Thread.later { progress.load() }
+      case _ =>
     }
   }