clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);

--- a/src/Pure/PIDE/document.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -760,7 +760,6 @@
 
     def get_text(range: Text.Range): Option[String]
 
-    def get_required(document: Boolean): Boolean
     def node_required: Boolean
 
     def get_blob: Option[Blob]

--- a/src/Pure/PIDE/document_editor.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -46,10 +46,36 @@
 
   sealed case class State(
     session_background: Option[Sessions.Background] = None,
+    selection: Set[Document.Node.Name] = Set.empty,
     views: Set[AnyRef] = Set.empty,
   ) {
     def is_active: Boolean = session_background.isDefined && views.nonEmpty
 
+    def is_required(name: Document.Node.Name): Boolean =
+      is_active && selection.contains(name) && all_document_theories.contains(name)
+
+    def required: List[Document.Node.Name] =
+      if (is_active) all_document_theories.filter(selection) else Nil
+
+    def all_document_theories: List[Document.Node.Name] =
+      session_background match {
+        case Some(background) => background.base.all_document_theories
+        case None => Nil
+      }
+
+    def select(
+      names: Iterable[Document.Node.Name],
+      set: Boolean = false,
+      toggle: Boolean = false
+    ): State = {
+      copy(selection =
+        names.foldLeft(selection) {
+          case (sel, name) =>
+            val b = if (toggle) !selection(name) else set
+            if (b) sel + name else sel - name
+        })
+    }
+
     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	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -20,21 +20,33 @@
   protected val document_editor: Synchronized[Document_Editor.State] =
     Synchronized(Document_Editor.State())
 
-  def document_session: Option[Sessions.Background] = document_editor.value.session_background
-  def document_active: Boolean = document_editor.value.is_active
-  def document_active_changed(): Unit = {}
-  private def document_editor_change(f: Document_Editor.State => Document_Editor.State): Unit = {
+  protected def document_state(): Document_Editor.State = document_editor.value
+
+  protected def document_state_changed(): Unit = {}
+  private def document_state_change(f: Document_Editor.State => Document_Editor.State): Unit = {
     val changed =
       document_editor.change_result { st =>
         val st1 = f(st)
-        (st.is_active != st1.is_active, st1)
+        (st.required != st1.required, st1)
       }
-    if (changed) document_active_changed()
+    if (changed) document_state_changed()
   }
+
+  def document_session(): Option[Sessions.Background] = document_state().session_background
+  def document_required(): List[Document.Node.Name] = document_state().required
+  def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name)
+
   def document_setup(background: Option[Sessions.Background]): Unit =
-    document_editor_change(_.copy(session_background = background))
-  def document_init(id: AnyRef): Unit = document_editor_change(_.register_view(id))
-  def document_exit(id: AnyRef): Unit = document_editor_change(_.unregister_view(id))
+    document_state_change(_.copy(session_background = background))
+
+  def document_select(
+    names: Iterable[Document.Node.Name],
+    set: Boolean = false,
+    toggle: Boolean = false
+  ): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
+
+  def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
+  def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))
 
 
   /* current situation */

--- a/src/Tools/VSCode/src/vscode_model.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -59,7 +59,7 @@
     node_name: Document.Node.Name
   ): VSCode_Model = {
     VSCode_Model(session, editor, node_name, Content.empty,
-      theory_required = File_Format.registry.is_theory(node_name))
+      node_required = File_Format.registry.is_theory(node_name))
   }
 }
 
@@ -70,8 +70,7 @@
   content: VSCode_Model.Content,
   version: Option[Long] = None,
   external_file: Boolean = false,
-  theory_required: Boolean = false,
-  document_required: Boolean = false,
+  node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
   pending_edits: List[Text.Edit] = Nil,
   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
@@ -79,14 +78,6 @@
 ) extends Document.Model {
   model =>
 
-  /* required */
-
-  def get_required(document: Boolean): Boolean =
-    if (document) document_required else theory_required
-
-  def node_required: Boolean = get_required(false)
-
-
   /* content */
 
   def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -117,6 +108,8 @@
     if (is_theory) {
       val snapshot = model.snapshot()
 
+      val required = node_required || editor.document_node_required(node_name)
+
       val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
       val caret_range =
         if (caret_perspective != 0) {
@@ -144,7 +137,7 @@
       val overlays = editor.node_overlays(node_name)
 
       (snapshot.node.load_commands_changed(doc_blobs),
-        Document.Node.Perspective(node_required, text_perspective, overlays))
+        Document.Node.Perspective(required, text_perspective, overlays))
     }
     else (false, Document.Node.Perspective_Text.empty)
   }

--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -182,15 +182,14 @@
 
   /* required nodes */
 
-  def required_nodes(document: Boolean): Set[Document.Node.Name] =
+  def nodes_required(): Set[Document.Node.Name] =
     (for {
       (node_name, model) <- state.value.models.iterator
-      if model.get_required(document)
+      if model.node_required
     } yield node_name).toSet
 
   def node_required(
     name: Document.Node.Name,
-    document: Boolean = false,
     toggle: Boolean = false,
     set: Boolean = false
   ) : Unit = {
@@ -201,13 +200,13 @@
         st.models.get(name) match {
           case None => (false, st)
           case Some(model) =>
-            val a = model.get_required(document)
+            val a = model.node_required
             val b = if (toggle) !a else set
             model match {
               case m: File_Model if a != b =>
-                (true, st.copy(models = st.models + (name -> m.set_required(document, b))))
+                (true, st.copy(models = st.models + (name -> m.set_node_required(b))))
               case m: Buffer_Model if a != b =>
-                m.set_required(document, b); (true, st)
+                m.set_node_required(b); (true, st)
               case _ => (false, st)
             }
         })
@@ -216,12 +215,11 @@
 
   def view_node_required(
     view: View,
-    document: Boolean = false,
     toggle: Boolean = false,
     set: Boolean = false
   ): Unit =
     Document_Model.get(view.getBuffer).foreach(model =>
-      node_required(model.node_name, document = document, toggle = toggle, set = set))
+      node_required(model.node_name, toggle = toggle, set = set))
 
 
   /* flushed edits */
@@ -334,9 +332,6 @@
 
   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
@@ -346,6 +341,8 @@
     if (JEdit_Options.continuous_checking() && is_theory) {
       val snapshot = this.snapshot()
 
+      val required = node_required || PIDE.editor.document_node_required(node_name)
+
       val reparse = snapshot.node.load_commands_changed(doc_blobs)
       val perspective =
         if (hidden) Text.Perspective.empty
@@ -356,7 +353,7 @@
         }
       val overlays = PIDE.editor.node_overlays(node_name)
 
-      (reparse, Document.Node.Perspective(node_required, perspective, overlays))
+      (reparse, Document.Node.Perspective(required, perspective, overlays))
     }
     else (false, Document.Node.Perspective_Text.empty)
   }
@@ -377,13 +374,12 @@
 object File_Model {
   def empty(session: Session): File_Model =
     File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
-      false, false, Document.Node.Perspective_Text.empty, Nil)
+      false, Document.Node.Perspective_Text.empty, Nil)
 
   def init(session: Session,
     node_name: Document.Node.Name,
     text: String,
-    theory_required: Boolean = false,
-    document_required: Boolean = false,
+    node_required: Boolean = false,
     last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
@@ -391,9 +387,8 @@
     file.foreach(PIDE.plugin.file_watcher.register_parent(_))
 
     val content = Document_Model.File_Content(text)
-    val theory_required1 = theory_required || File_Format.registry.is_theory(node_name)
-    File_Model(session, node_name, file, content, theory_required1, document_required,
-      last_perspective, pending_edits)
+    val node_required1 = node_required || File_Format.registry.is_theory(node_name)
+    File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
   }
 }
 
@@ -402,18 +397,13 @@
   node_name: Document.Node.Name,
   file: Option[JFile],
   content: Document_Model.File_Content,
-  theory_required: Boolean,
-  document_required: Boolean,
+  node_required: Boolean,
   last_perspective: Document.Node.Perspective_Text.T,
   pending_edits: List[Text.Edit]
 ) extends Document_Model {
   /* required */
 
-  def get_required(document: Boolean): Boolean =
-    if (document) document_required else theory_required
-
-  def set_required(document: Boolean, b: Boolean): File_Model =
-    if (document) copy(document_required = b) else copy(theory_required = b)
+  def set_node_required(b: Boolean): File_Model = copy(node_required = b)
 
 
   /* text */
@@ -505,13 +495,9 @@
   /* perspective */
 
   // owned by GUI thread
-  private var _theory_required = false
-  private var _document_required = false
-
-  def get_required(document: Boolean): Boolean =
-    if (document) _document_required else _theory_required
-  def set_required(document: Boolean, b: Boolean): Unit =
-    GUI_Thread.require { if (document) _document_required = b else _theory_required = b }
+  private var _node_required = false
+  def node_required: Boolean = _node_required
+  def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
 
   def document_view_iterator: Iterator[Document_View] =
     for {
@@ -683,8 +669,7 @@
       case None =>
         pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))))
       case Some(file_model) =>
-        set_required(false, file_model.theory_required)
-        set_required(true, file_model.document_required)
+        set_node_required(file_model.node_required)
         pending_edits.set_last_perspective(file_model.last_perspective)
         pending_edits.edit(
           file_model.pending_edits :::
@@ -707,8 +692,7 @@
     init_token_marker()
 
     File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer),
-      theory_required = _theory_required,
-      document_required = _document_required,
+      node_required = _node_required,
       last_perspective = pending_edits.get_last_perspective,
       pending_edits = pending_edits.get_edits)
   }

--- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -61,7 +61,7 @@
     session.global_options.post(Session.Global_Options(PIDE.options.value))
   }
 
-  override def document_active_changed(): Unit = state_changed()
+  override def document_state_changed(): Unit = state_changed()
 
 
   /* current situation */

--- a/src/Tools/jEdit/src/theories_status.scala	Mon Dec 19 15:29:24 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Tue Dec 20 13:59:07 2022 +0100
@@ -28,8 +28,8 @@
   private var document_required = Set.empty[Document.Node.Name]
 
   private def init_state(): Unit = GUI_Thread.require {
-    theory_required = Document_Model.required_nodes(false)
-    document_required = Document_Model.required_nodes(true)
+    theory_required = Document_Model.nodes_required()
+    document_required = PIDE.editor.document_required().toSet
   }
 
 
@@ -156,8 +156,8 @@
       component.label_border(name)
       component.label.text =
         name.theory_base_name +
-        (if (!document && PIDE.editor.document_active && document_required.contains(name))
-          document_marker else no_document_marker)
+        (if (!document && PIDE.editor.document_node_required(name)) document_marker
+         else no_document_marker)
       component
     }
   }
@@ -183,7 +183,9 @@
           val index_location = peer.indexToLocation(index)
           if (node_renderer.in_required(index_location, point)) {
             if (clicks == 1) {
-              Document_Model.node_required(listData(index), toggle = true, document = document)
+              val name = listData(index)
+              if (document) PIDE.editor.document_select(Set(name), toggle = true)
+              else Document_Model.node_required(name, toggle = true)
             }
           }
           else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)