clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
--- a/src/Pure/PIDE/document.scala Mon Dec 19 11:42:45 2022 +0100
+++ b/src/Pure/PIDE/document.scala Mon Dec 19 12:22:47 2022 +0100
@@ -761,7 +761,7 @@
def get_text(range: Text.Range): Option[String]
def get_required(document: Boolean): Boolean
- def node_required: Boolean = get_required(false) || get_required(true)
+ def node_required: Boolean
def get_blob: Option[Blob]
def bibtex_entries: List[Text.Info[String]]
--- a/src/Tools/VSCode/src/vscode_model.scala Mon Dec 19 11:42:45 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala Mon Dec 19 12:22:47 2022 +0100
@@ -84,6 +84,8 @@
def get_required(document: Boolean): Boolean =
if (document) document_required else theory_required
+ def node_required: Boolean = get_required(false)
+
/* content */
--- a/src/Tools/jEdit/src/document_model.scala Mon Dec 19 11:42:45 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 19 12:22:47 2022 +0100
@@ -337,6 +337,9 @@
def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil
+ def node_required: Boolean =
+ get_required(false) || PIDE.editor.document_active && get_required(true)
+
def node_perspective(
doc_blobs: Document.Blobs,
hidden: Boolean