src/Pure/PIDE/editor.scala
changeset 77142 139a0119ae3c
parent 77029 1046a69fabaa
child 77144 42c3970e1ac1
--- 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()