src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sun Nov 06 23:10:28 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Nov 07 21:32:09 2022 +0100
@@ -761,7 +761,9 @@
 
     def get_text(range: Text.Range): Option[String]
 
-    def node_required: Boolean
+    def get_required(document: Boolean): Boolean
+    def node_required: Boolean = get_required(false) || get_required(true)
+
     def get_blob: Option[Blob]
     def bibtex_entries: List[Text.Info[String]]