# HG changeset patch
# User wenzelm
# Date 1675092017 -3600
# Node ID 139a0119ae3c0e6393d372719b3017dceec3db66
# Parent  79231a210f5d17bceb6a03f7a1336b93f8505a25
clarified operation (without change of signature!);

diff -r 79231a210f5d -r 139a0119ae3c src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Mon Jan 30 15:02:38 2023 +0100
+++ b/src/Pure/PIDE/editor.scala	Mon Jan 30 16:20:17 2023 +0100
@@ -37,7 +37,8 @@
     if (changed) document_state_changed()
   }
 
-  def document_session(): Option[Sessions.Background] = document_state().session_background
+  def document_session(): Option[Sessions.Background] =
+    document_state().session_background.filter(_.info.documents.nonEmpty)
 
   def document_required(): List[Document.Node.Name] = {
     val st = document_state()
diff -r 79231a210f5d -r 139a0119ae3c src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Mon Jan 30 15:02:38 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Mon Jan 30 16:20:17 2023 +0100
@@ -225,7 +225,7 @@
 
   private def build_document(): Unit = {
     PIDE.editor.document_session() match {
-      case Some(session_background) if session_background.info.documents.nonEmpty =>
+      case Some(session_background) =>
         run_process(only_running = true) { progress =>
           show_page(output_page)
           val result = Exn.capture { document_build(session_background, progress) }
@@ -246,7 +246,7 @@
           show_state()
           show_page(if (Exn.is_interrupt_exn(result)) input_page else output_page)
         }
-      case _ =>
+      case None =>
     }
   }