src/Pure/PIDE/editor.scala

--- a/src/Pure/PIDE/editor.scala	Mon Jan 30 16:26:10 2023 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Jan 31 12:27:00 2023 +0100
@@ -37,8 +37,8 @@
     if (changed) document_state_changed()
   }
 
-  def document_session(): Option[Sessions.Background] =
-    document_state().session_background.filter(_.info.documents.nonEmpty)
+  def document_session(): Document_Editor.Session =
+    document_state().session(() => session.snapshot())
 
   def document_required(): List[Document.Node.Name] = {
     val st = document_state()