clarified signature;

--- a/src/Pure/PIDE/document_editor.scala	Sun Dec 18 14:39:35 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Sun Dec 18 15:49:37 2022 +0100
@@ -45,10 +45,10 @@
   /* global state */
 
   sealed case class State(
-    session_info: Option[Sessions.Info] = None,
+    session_background: Option[Sessions.Background] = None,
     views: Set[AnyRef] = Set.empty,
   ) {
-    def is_active: Boolean = session_info.isDefined && views.nonEmpty
+    def is_active: Boolean = session_background.isDefined && views.nonEmpty
 
     def register_view(id: AnyRef): State = copy(views = views + id)
     def unregister_view(id: AnyRef): State = copy(views = views - id)

--- a/src/Pure/PIDE/editor.scala	Sun Dec 18 14:39:35 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Sun Dec 18 15:49:37 2022 +0100
@@ -20,8 +20,12 @@
   protected val document_editor: Synchronized[Document_Editor.State] =
     Synchronized(Document_Editor.State())
 
+  def document_editor_session: Option[Sessions.Background] =
+    document_editor.value.session_background
   def document_editor_active: Boolean =
     document_editor.value.is_active
+  def document_editor_setup(background: Option[Sessions.Background]): Unit =
+    document_editor.change(_.copy(session_background = background))
   def document_editor_init(id: AnyRef): Unit =
     document_editor.change(_.register_view(id))
   def document_editor_exit(id: AnyRef): Unit =