--- a/src/Pure/PIDE/document_editor.scala Thu Dec 08 22:04:28 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Thu Dec 08 22:11:36 2022 +0100
@@ -41,4 +41,17 @@
GUI_Thread.later { update() }
}
+
+
+ /* global state */
+
+ sealed case class State(
+ session_info: Option[Sessions.Info] = None,
+ views: Set[AnyRef] = Set.empty,
+ ) {
+ def is_active: Boolean = session_info.isDefined && views.nonEmpty
+
+ def register_view(id: AnyRef): State = copy(views = views + id)
+ def unregister_view(id: AnyRef): State = copy(views = views - id)
+ }
}