clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
authorwenzelm
Mon, 19 Dec 2022 12:22:47 +0100
changeset 76703 8fac11f7f0f4
parent 76702 94cdf6513f01
child 76704 26f939b23fdd
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
src/Pure/PIDE/document.scala
src/Tools/VSCode/src/vscode_model.scala
src/Tools/jEdit/src/document_model.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]]
--- 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