# HG changeset patch
# User wenzelm
# Date 1671448967 -3600
# Node ID 8fac11f7f0f40b7d0290f2c72fd7268d2126d82d
# Parent  94cdf6513f01b471e3c6410f237326eb848f7f56
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);

diff -r 94cdf6513f01 -r 8fac11f7f0f4 src/Pure/PIDE/document.scala
--- 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]]
diff -r 94cdf6513f01 -r 8fac11f7f0f4 src/Tools/VSCode/src/vscode_model.scala
--- 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 */
 
diff -r 94cdf6513f01 -r 8fac11f7f0f4 src/Tools/jEdit/src/document_model.scala
--- 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