maintain global state of document editor views, notably for is_active operation;

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

--- a/src/Pure/PIDE/editor.scala	Thu Dec 08 22:04:28 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Thu Dec 08 22:11:36 2022 +0100
@@ -15,6 +15,19 @@
   def invoke(): Unit
 
 
+  /* document editor */
+
+  protected val document_editor: Synchronized[Document_Editor.State] =
+    Synchronized(Document_Editor.State())
+
+  def document_editor_active: Boolean =
+    document_editor.value.is_active
+  def document_editor_init(id: AnyRef): Unit =
+    document_editor.change(_.register_view(id))
+  def document_editor_exit(id: AnyRef): Unit =
+    document_editor.change(_.unregister_view(id))
+
+
   /* current situation */
 
   def current_node(context: Context): Option[Document.Node.Name]

--- a/src/Tools/jEdit/src/document_dockable.scala	Thu Dec 08 22:04:28 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Thu Dec 08 22:11:36 2022 +0100
@@ -44,6 +44,8 @@
 }
 
 class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
+  dockable =>
+
   GUI_Thread.require {}
 
 
@@ -243,6 +245,7 @@
     }
 
   override def init(): Unit = {
+    PIDE.editor.document_editor_init(dockable)
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
@@ -255,5 +258,6 @@
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     delay_resize.revoke()
+    PIDE.editor.document_editor_exit(dockable)
   }
 }