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()