clarified state document nodes for Theories_Status / Document_Dockable;

--- a/src/Pure/PIDE/document_editor.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -63,6 +63,9 @@
         case None => Nil
       }
 
+    def active_document_theories: List[Document.Node.Name] =
+      if (is_active) all_document_theories else Nil
+
     def select(
       names: Iterable[Document.Node.Name],
       set: Boolean = false,

--- a/src/Pure/PIDE/document_status.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Pure/PIDE/document_status.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -97,6 +97,20 @@
   /* node status */
 
   object Node_Status {
+    val empty: Node_Status =
+      Node_Status(
+        is_suppressed = false,
+        unprocessed = 0,
+        running = 0,
+        warned = 0,
+        failed = 0,
+        finished = 0,
+        canceled = false,
+        terminated = false,
+        initialized = false,
+        finalized = false,
+        consolidated = false)
+
     def make(
       state: Document.State,
       version: Document.Version,
@@ -157,6 +171,8 @@
     finalized: Boolean,
     consolidated: Boolean
   ) {
+    def is_empty: Boolean = this == Node_Status.empty
+
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
 
@@ -230,11 +246,12 @@
     def apply(name: Document.Node.Name): Node_Status = rep(name)
     def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
 
-    def present: List[(Document.Node.Name, Node_Status)] =
-      (for {
-        name <- nodes.topological_order.iterator
-        node_status <- get(name)
-      } yield (name, node_status)).toList
+    def present(
+      domain: Option[List[Document.Node.Name]] = None
+    ): List[(Document.Node.Name, Node_Status)] = {
+      for (name <- domain.getOrElse(nodes.topological_order))
+        yield name -> get(name).getOrElse(Node_Status.empty)
+    }
 
     def quasi_consolidated(name: Document.Node.Name): Boolean =
       rep.get(name) match {

--- a/src/Pure/PIDE/editor.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -36,6 +36,8 @@
   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_theories(): List[Document.Node.Name] = document_state().active_document_theories
+
   def document_setup(background: Option[Sessions.Background]): Unit =
     document_state_change(_.copy(session_background = background))
 

--- a/src/Pure/PIDE/headless.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -390,8 +390,9 @@
 
                   val theory_progress =
                     (for {
-                      (name, node_status) <- st1.nodes_status.present.iterator
-                      if changed_st.changed_nodes(name) && !st.already_committed.isDefinedAt(name)
+                      (name, node_status) <- st1.nodes_status.present().iterator
+                      if !node_status.is_empty && changed_st.changed_nodes(name) &&
+                        !st.already_committed.isDefinedAt(name)
                       p1 = node_status.percentage
                       if p1 > 0 && !st.nodes_status.get(name).map(_.percentage).contains(p1)
                     } yield Progress.Theory(name.theory, percentage = Some(p1))).toList

--- a/src/Pure/Tools/server.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Pure/Tools/server.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -269,7 +269,7 @@
 
     override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
       val json =
-        for ((name, node_status) <- nodes_status.present)
+        for ((name, node_status) <- nodes_status.present() if !node_status.is_empty)
           yield name.json + ("status" -> node_status.json)
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }

--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -206,7 +206,10 @@
     state.change_result { st =>
       val stable_tip_version = session.stable_tip_version(st.models)
 
-      val thy_files = resources.resolve_dependencies(st.models, Nil)
+      val thy_files =
+        resources.resolve_dependencies(st.models,
+          editor.document_required().map((_, Position.none)))
+
       val aux_files = stable_tip_version.toList.flatMap(undefined_blobs)
 
       val loaded_models =

--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -121,12 +121,18 @@
 
   /* document build process */
 
+  private def document_theories(): List[Document.Node.Name] =
+    PIDE.editor.document_theories()
+
   private def cancel(): Unit =
     current_state.change { st => st.process.cancel(); st }
 
   private def init_state(): Unit =
     current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
 
+  private def process_finished(): Unit =
+    current_state.change(_.copy(process = Future.value(())))
+
   private def load_document(session: String): Boolean = {
     current_state.change_result { st =>
       if (st.process.is_finished) {
@@ -139,11 +145,19 @@
                 Document_Build.session_background(
                   options, session, dirs = JEdit_Sessions.session_dirs)
               PIDE.editor.document_setup(Some(session_background))
-              GUI_Thread.later { show_state(); show_page(theories_page) }
+
+              process_finished()
+              GUI_Thread.later {
+                theories.update(domain = Some(document_theories().toSet), trim = true)
+                show_state()
+                show_page(theories_page)
+              }
             }
             catch {
               case exn: Throwable if !Exn.is_interrupt(exn) =>
                 current_state.change(_.finish(Protocol.error_message(Exn.print(exn))))
+
+                process_finished()
                 GUI_Thread.later { show_state(); show_page(output_page) }
             }
           }
@@ -178,6 +192,8 @@
                 case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
               }
             current_state.change(_.finish(msg))
+            process_finished()
+
             show_state()
 
             show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
@@ -272,7 +288,8 @@
         }
       case changed: Session.Commands_Changed =>
         GUI_Thread.later {
-          theories.update(domain = Some(changed.nodes), trim = changed.assignment)
+          val domain = document_theories().filter(changed.nodes).toSet
+          if (domain.nonEmpty) theories.update(domain = Some(domain))
         }
     }
 
@@ -281,7 +298,7 @@
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
-    theories.update()
+    theories.update(domain = Some(document_theories().toSet), force = true)
     handle_resize()
     delay_load.invoke()
   }

--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -112,7 +112,9 @@
     val required_files = {
       val models = Document_Model.get_models()
 
-      val thy_files = resources.resolve_dependencies(models, Nil)
+      val thy_files =
+        resources.resolve_dependencies(models,
+          PIDE.editor.document_required().map((_, Position.none)))
 
       val aux_files =
         if (resources.auto_resolve) {

--- a/src/Tools/jEdit/src/theories_status.scala	Tue Dec 20 13:59:07 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Tue Dec 20 16:34:13 2022 +0100
@@ -24,12 +24,19 @@
   /* component state -- owned by GUI thread */
 
   private var nodes_status = Document_Status.Nodes_Status.empty
-  private var theory_required = Set.empty[Document.Node.Name]
+  private var nodes_required = Set.empty[Document.Node.Name]
   private var document_required = Set.empty[Document.Node.Name]
+  private var document_theories = List.empty[Document.Node.Name]
 
   private def init_state(): Unit = GUI_Thread.require {
-    theory_required = Document_Model.nodes_required()
-    document_required = PIDE.editor.document_required().toSet
+    if (document) {
+      nodes_required = PIDE.editor.document_required().toSet
+      document_theories = PIDE.editor.document_theories()
+    }
+    else {
+      nodes_required = Document_Model.nodes_required()
+      document_required = PIDE.editor.document_required().toSet
+    }
   }
 
 
@@ -151,13 +158,11 @@
       index: Int
     ): Component = {
       component.node_name = name
-      component.required.selected =
-        (if (document) document_required else theory_required).contains(name)
+      component.required.selected = nodes_required.contains(name)
       component.label_border(name)
       component.label.text =
         name.theory_base_name +
-        (if (!document && PIDE.editor.document_node_required(name)) document_marker
-         else no_document_marker)
+        (if (document_required.contains(name)) document_marker else no_document_marker)
       component
     }
   }
@@ -216,7 +221,11 @@
 
   /* update */
 
-  def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = {
+  def update(
+    domain: Option[Set[Document.Node.Name]] = None,
+    trim: Boolean = false,
+    force: Boolean = false
+  ): Unit = {
     GUI_Thread.require {}
 
     val snapshot = PIDE.session.snapshot()
@@ -226,12 +235,15 @@
         PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
 
     nodes_status = nodes_status1
-    if (nodes_status_changed) {
+    if (nodes_status_changed || force) {
       gui.listData =
-        (for {
-          (name, node_status) <- nodes_status1.present.iterator
-          if !node_status.is_suppressed && node_status.total > 0
-        } yield name).toList
+        if (document) nodes_status1.present(domain = Some(document_theories)).map(_._1)
+        else {
+          (for {
+            (name, node_status) <- nodes_status1.present().iterator
+            if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0
+          } yield name).toList
+        }
     }
   }