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