# HG changeset patch
# User wenzelm
# Date 1671561835 -3600
# Node ID 5364cdc3ec0ed2b5562f989a4150d073b75fa588
# Parent  c48fe2be847f09efc9a5e8364dbf0329c399a0ef# Parent  37f7b2965e02ada0db0373b58d106874b470ab7f
merged

diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -13,13 +13,15 @@
 object GUI_Thread {
   /* context check */
 
+  def check(): Boolean = SwingUtilities.isEventDispatchThread()
+
   def assert[A](body: => A): A = {
-    Predef.assert(SwingUtilities.isEventDispatchThread)
+    Predef.assert(check())
     body
   }
 
   def require[A](body: => A): A = {
-    Predef.require(SwingUtilities.isEventDispatchThread, "GUI thread expected")
+    Predef.require(check(), "GUI thread expected")
     body
   }
 
@@ -27,7 +29,7 @@
   /* event dispatch queue */
 
   def now[A](body: => A): A = {
-    if (SwingUtilities.isEventDispatchThread) body
+    if (check()) body
     else {
       lazy val result = assert { Exn.capture(body) }
       SwingUtilities.invokeAndWait(() => result)
@@ -36,12 +38,12 @@
   }
 
   def later(body: => Unit): Unit = {
-    if (SwingUtilities.isEventDispatchThread) body
+    if (check()) body
     else SwingUtilities.invokeLater(() => body)
   }
 
   def future[A](body: => A): Future[A] = {
-    if (SwingUtilities.isEventDispatchThread) Future.value(body)
+    if (check()) Future.value(body)
     else {
       val promise = Future.promise[A]
       later { promise.fulfill_result(Exn.capture(body)) }
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document.ML	Tue Dec 20 19:43:55 2022 +0100
@@ -85,12 +85,13 @@
 
 val no_header: node_header =
   {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
-val no_perspective = make_perspective (false, [], []);
+
+val empty_perspective = make_perspective (false, [], []);
 
 val empty_node =
-  make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
+  make_node (no_header, NONE, empty_perspective, Entries.empty, NONE, Lazy.value ());
 
-fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
+fun is_empty_perspective ({required, visible, visible_last, overlays}: perspective) =
   not required andalso
   Inttab.is_empty visible andalso
   is_none visible_last andalso
@@ -99,7 +100,7 @@
 fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
   header = no_header andalso
   is_none keywords andalso
-  is_no_perspective perspective andalso
+  is_empty_perspective perspective andalso
   Entries.is_empty entries andalso
   is_none result andalso
   Lazy.is_finished consolidated;
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -181,24 +181,23 @@
 
     /* perspective */
 
-    type Perspective_Text = Perspective[Text.Edit, Text.Perspective]
-    type Perspective_Command = Perspective[Command.Edit, Command.Perspective]
-
-    val no_perspective_text: Perspective_Text =
-      Perspective(false, Text.Perspective.empty, Overlays.empty)
-
-    val no_perspective_command: Perspective_Command =
-      Perspective(false, Command.Perspective.empty, Overlays.empty)
+    object Perspective_Text {
+      type T = Perspective[Text.Edit, Text.Perspective]
+      val empty: T = Perspective(false, Text.Perspective.empty, Overlays.empty)
+      def is_empty(perspective: T): Boolean =
+        !perspective.required &&
+        perspective.visible.is_empty &&
+        perspective.overlays.is_empty
+    }
 
-    def is_no_perspective_text(perspective: Perspective_Text): Boolean =
-      !perspective.required &&
-      perspective.visible.is_empty &&
-      perspective.overlays.is_empty
-
-    def is_no_perspective_command(perspective: Perspective_Command): Boolean =
-      !perspective.required &&
-      perspective.visible.is_empty &&
-      perspective.overlays.is_empty
+    object Perspective_Command {
+      type T = Perspective[Command.Edit, Command.Perspective]
+      val empty: T = Perspective(false, Command.Perspective.empty, Overlays.empty)
+      def is_empty(perspective: T): Boolean =
+        !perspective.required &&
+        perspective.visible.is_empty &&
+        perspective.overlays.is_empty
+    }
 
 
     /* commands */
@@ -272,14 +271,14 @@
     val header: Node.Header = Node.no_header,
     val syntax: Option[Outer_Syntax] = None,
     val text_perspective: Text.Perspective = Text.Perspective.empty,
-    val perspective: Node.Perspective_Command = Node.no_perspective_command,
+    val perspective: Node.Perspective_Command.T = Node.Perspective_Command.empty,
     _commands: Node.Commands = Node.Commands.empty
   ) {
     def is_empty: Boolean =
       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
-      Node.is_no_perspective_command(perspective) &&
+      Node.Perspective_Command.is_empty(perspective) &&
       commands.isEmpty
 
     def has_header: Boolean = header != Node.no_header
@@ -304,7 +303,7 @@
 
     def update_perspective(
         new_text_perspective: Text.Perspective,
-        new_perspective: Node.Perspective_Command): Node =
+        new_perspective: Node.Perspective_Command.T): Node =
       new Node(get_blob, header, syntax, new_text_perspective, new_perspective, _commands)
 
     def edit_perspective: Node.Edit[Text.Edit, Text.Perspective] =
@@ -312,7 +311,7 @@
 
     def same_perspective(
         other_text_perspective: Text.Perspective,
-        other_perspective: Node.Perspective_Command): Boolean =
+        other_perspective: Node.Perspective_Command.T): Boolean =
       text_perspective == other_text_perspective &&
       perspective.required == other_perspective.required &&
       perspective.visible.same(other_perspective.visible) &&
@@ -761,8 +760,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]]
@@ -770,7 +768,7 @@
     def node_edits(
       node_header: Node.Header,
       text_edits: List[Text.Edit],
-      perspective: Node.Perspective_Text
+      perspective: Node.Perspective_Text.T
     ): List[Edit_Text] = {
       val edits: List[Node.Edit[Text.Edit, Text.Perspective]] =
         get_blob match {
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/document_editor.scala
--- a/src/Pure/PIDE/document_editor.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -46,10 +46,39 @@
 
   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 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,
+      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)
   }
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/document_status.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -97,10 +97,25 @@
   /* 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,
-      name: Document.Node.Name): Node_Status = {
+      name: Document.Node.Name
+    ): Node_Status = {
       val node = version.nodes(name)
 
       var unprocessed = 0
@@ -156,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
 
@@ -229,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 {
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/editor.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -20,16 +20,38 @@
   protected val document_editor: Synchronized[Document_Editor.State] =
     Synchronized(Document_Editor.State())
 
-  def document_editor_session: Option[Sessions.Background] =
-    document_editor.value.session_background
-  def document_editor_active: Boolean =
-    document_editor.value.is_active
-  def document_editor_setup(background: Option[Sessions.Background]): Unit =
-    document_editor.change(_.copy(session_background = background))
-  def document_editor_init(id: AnyRef): Unit =
-    document_editor.change(_.register_view(id))
-  def document_editor_exit(id: AnyRef): Unit =
-    document_editor.change(_.unregister_view(id))
+  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.required != st1.required, st1)
+      }
+    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_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))
+
+  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_select_all(set: Boolean = false): Unit =
+    document_state_change(st => st.select(st.active_document_theories, set = set))
+
+  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 */
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/PIDE/headless.scala	Tue Dec 20 19:43:55 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
@@ -471,7 +472,7 @@
     ) {
       override def toString: String = node_name.toString
 
-      def node_perspective: Document.Node.Perspective_Text =
+      def node_perspective: Document.Node.Perspective_Text.T =
         Document.Node.Perspective(node_required, Text.Perspective.empty, Document.Node.Overlays.empty)
 
       def make_edits(text_edits: List[Text.Edit]): List[Document.Edit_Text] =
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -115,10 +115,11 @@
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
-    progress: Progress = new Progress
+    progress: Progress = new Progress,
+    verbose: Boolean = false
   ): Sessions.Background = {
       Sessions.load_structure(options + "document=pdf", dirs = dirs).
-        selection_deps(Sessions.Selection.session(session), progress = progress).
+        selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
         background(session)
   }
 
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -258,7 +258,7 @@
 
       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
-        val perspective: Document.Node.Perspective_Command =
+        val perspective: Document.Node.Perspective_Command.T =
           Document.Node.Perspective(required, visible_overlay, overlays)
         if (node.same_perspective(text_perspective, perspective)) node
         else {
diff -r c48fe2be847f -r 5364cdc3ec0e src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Pure/Tools/server.scala	Tue Dec 20 19:43:55 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))
     }
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/VSCode/src/vscode_model.scala
--- a/src/Tools/VSCode/src/vscode_model.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_model.scala	Tue Dec 20 19:43:55 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,21 +70,14 @@
   content: VSCode_Model.Content,
   version: Option[Long] = None,
   external_file: Boolean = false,
-  theory_required: Boolean = false,
-  document_required: Boolean = false,
-  last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+  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,
   published_decorations: List[VSCode_Model.Decoration] = Nil
 ) extends Document.Model {
   model =>
 
-  /* required */
-
-  def get_required(document: Boolean): Boolean =
-    if (document) document_required else theory_required
-
-
   /* content */
 
   def get_text(range: Text.Range): Option[String] = content.doc.get_text(range)
@@ -111,10 +104,12 @@
   def node_perspective(
     doc_blobs: Document.Blobs,
     caret: Option[Line.Position]
-  ): (Boolean, Document.Node.Perspective_Text) = {
+  ): (Boolean, Document.Node.Perspective_Text.T) = {
     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) {
@@ -142,9 +137,9 @@
       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.no_perspective_text)
+    else (false, Document.Node.Perspective_Text.empty)
   }
 
 
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Dec 20 19:43:55 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 =
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -27,10 +27,6 @@
     val FINISHED = Value("finished")
   }
 
-  sealed case class Result(output: List[XML.Tree] = Nil) {
-    def failed: Boolean = output.exists(Protocol.is_error)
-  }
-
   object State {
     def init(): State = State()
   }
@@ -44,8 +40,10 @@
     def run(progress: Progress, process: Future[Unit]): State =
       copy(progress = progress, process = process, status = Status.RUNNING)
 
-    def finish(result: Result): State = State(output = result.output)
-    def finish(msg: XML.Tree): State = finish(Result(output = List(msg)))
+    def finish(output: List[XML.Tree]): State =
+      copy(process = Future.value(()), status = Status.FINISHED, output = output)
+
+    def ok: Boolean = !output.exists(Protocol.is_error)
   }
 }
 
@@ -121,73 +119,91 @@
 
   /* document build process */
 
-  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 cancel_process(): Unit =
+    current_state.change { st => st.process.cancel(); st }
+
+  private def await_process(): Unit =
+    current_state.guarded_access(st => if (st.process.is_finished) None else Some((), st))
+
+  private def finish_process(output: List[XML.Tree]): Unit =
+    current_state.change(_.finish(output))
+
+  private def run_process(body: Document_Editor.Log_Progress => Unit): Boolean = {
+    val started =
+      current_state.change_result { st =>
+        if (st.process.is_finished) {
+          val progress = log_progress()
+          val process =
+            Future.thread[Unit](name = "Document_Dockable.process") {
+              await_process()
+              body(progress)
+            }
+          (true, st.run(progress, process))
+        }
+        else (false, st)
+      }
+    show_state()
+    started
+  }
+
   private def load_document(session: String): Boolean = {
-    current_state.change_result { st =>
-      if (st.process.is_finished) {
-        val options = PIDE.options.value
-        val progress = log_progress()
-        val process =
-          Future.thread[Unit](name = "Document_Dockable.load_document") {
-            try {
-              val session_background =
-                Document_Build.session_background(
-                  options, session, dirs = JEdit_Sessions.session_dirs)
-              PIDE.editor.document_editor_setup(Some(session_background))
-              GUI_Thread.later { show_state(); show_page(theories_page) }
-            }
-            catch {
-              case exn: Throwable if !Exn.is_interrupt(exn) =>
-                current_state.change(_.finish(Protocol.error_message(Exn.message(exn))))
-                GUI_Thread.later { show_state(); show_page(output_page) }
-            }
+    val options = PIDE.options.value
+    run_process { progress =>
+      try {
+        val session_background =
+          Document_Build.session_background(
+            options, session, dirs = JEdit_Sessions.session_dirs)
+        PIDE.editor.document_setup(Some(session_background))
+
+        finish_process(Nil)
+        GUI_Thread.later {
+          val domain = PIDE.editor.document_theories().toSet
+          theories.update(domain = Some(domain), trim = true, force = true)
+          show_state()
+          show_page(theories_page)
+        }
+      }
+      catch {
+        case exn: Throwable if !Exn.is_interrupt(exn) =>
+          finish_process(List(Protocol.error_message(Exn.print(exn))))
+          GUI_Thread.later {
+            show_state()
+            show_page(output_page)
           }
-        (true, st.run(progress, process))
       }
-      else (false, st)
     }
   }
 
   private def build_document(): Unit = {
-    current_state.change { st =>
-      if (st.process.is_finished) {
-        val progress = log_progress()
-        val process =
-          Future.thread[Unit](name = "Document_Dockable.build_document") {
-            show_page(theories_page)
-            Time.seconds(2.0).sleep()
+    run_process { progress =>
+      show_page(theories_page)
+      Time.seconds(2.0).sleep()
 
-            show_page(log_page)
-            val res =
-              Exn.capture {
-                progress.echo("Start " + Date.now())
-                for (i <- 1 to 200) {
-                  progress.echo("message " + i)
-                  Time.seconds(0.1).sleep()
-                }
-                progress.echo("Stop " + Date.now())
-              }
-            val msg =
-              res match {
-                case Exn.Res(_) => Protocol.writeln_message("OK")
-                case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
-              }
-            current_state.change(_.finish(msg))
-            show_state()
+      show_page(log_page)
+      val res =
+        Exn.capture {
+          progress.echo("Start " + Date.now())
+          for (i <- 1 to 200) {
+            progress.echo("message " + i)
+            Time.seconds(0.1).sleep()
+          }
+          progress.echo("Stop " + Date.now())
+        }
+      val msg =
+        res match {
+          case Exn.Res(_) => Protocol.writeln_message("OK")
+          case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
+        }
+      finish_process(List(msg))
 
-            show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
-            GUI_Thread.later { progress.load() }
-          }
-        st.run(progress, process)
-      }
-      else st
+      show_state()
+
+      show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
+      GUI_Thread.later { progress.load() }
     }
-    show_state()
   }
 
 
@@ -214,7 +230,7 @@
   private val cancel_button =
     new GUI.Button("Cancel") {
       tooltip = "Cancel build process"
-      override def clicked(): Unit = cancel()
+      override def clicked(): Unit = cancel_process()
     }
 
   private val view_button =
@@ -234,10 +250,26 @@
 
   /* message pane with pages */
 
+  private val select_all_button =
+    new GUI.Button("All") {
+      tooltip = "Select all document theories"
+      override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
+    }
+
+  private val select_none_button =
+    new GUI.Button("None") {
+      tooltip = "Deselect all document theories"
+      override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
+    }
+
+  private val theories_controls =
+    Wrap_Panel(List(select_all_button, select_none_button))
+
   private val theories = new Theories_Status(view, document = true)
 
   private val theories_page =
     new TabbedPane.Page("Theories", new BorderPanel {
+      layout(theories_controls) = BorderPanel.Position.North
       layout(theories.gui) = BorderPanel.Position.Center
     }, "Selection and status of document theories")
 
@@ -268,20 +300,20 @@
         GUI_Thread.later {
           document_session.load()
           handle_resize()
-          theories.reinit()
+          theories.refresh()
         }
       case changed: Session.Commands_Changed =>
         GUI_Thread.later {
-          theories.update(domain = Some(changed.nodes), trim = changed.assignment)
+          val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
+          if (domain.nonEmpty) theories.update(domain = Some(domain))
         }
     }
 
   override def init(): Unit = {
-    PIDE.editor.document_editor_init(dockable)
+    PIDE.editor.document_init(dockable)
     init_state()
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
-    theories.update()
     handle_resize()
     delay_load.invoke()
   }
@@ -290,6 +322,6 @@
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     delay_resize.revoke()
-    PIDE.editor.document_editor_exit(dockable)
+    PIDE.editor.document_exit(dockable)
   }
 }
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 20 19:43:55 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,30 +200,26 @@
         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)
             }
         })
-    if (changed) {
-      PIDE.plugin.options_changed()
-      PIDE.editor.flush()
-    }
+    if (changed) PIDE.editor.state_changed()
   }
 
   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 */
@@ -340,12 +335,14 @@
   def node_perspective(
     doc_blobs: Document.Blobs,
     hidden: Boolean
-  ): (Boolean, Document.Node.Perspective_Text) = {
+  ): (Boolean, Document.Node.Perspective_Text.T) = {
     GUI_Thread.require {}
 
     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,9 +353,9 @@
         }
       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.no_perspective_text)
+    else (false, Document.Node.Perspective_Text.empty)
   }
 
 
@@ -377,23 +374,21 @@
 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.no_perspective_text, 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,
-    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
+    node_required: Boolean = false,
+    last_perspective: Document.Node.Perspective_Text.T = Document.Node.Perspective_Text.empty,
     pending_edits: List[Text.Edit] = Nil
   ): File_Model = {
     val file = JEdit_Lib.check_file(node_name.node)
     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,
-  last_perspective: Document.Node.Perspective_Text,
+  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 */
@@ -469,10 +459,10 @@
   def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
     if (pending_edits.nonEmpty ||
         !File_Format.registry.is_theory(node_name) &&
-          (node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
+          (node_required || !Document.Node.Perspective_Text.is_empty(last_perspective))) None
     else {
       val text_edits = List(Text.Edit.remove(0, content.text))
-      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
+      Some(node_edits(Document.Node.no_header, text_edits, Document.Node.Perspective_Text.empty))
     }
 
 
@@ -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 {
@@ -586,12 +572,12 @@
 
   private object pending_edits {
     private val pending = new mutable.ListBuffer[Text.Edit]
-    private var last_perspective = Document.Node.no_perspective_text
+    private var last_perspective = Document.Node.Perspective_Text.empty
 
     def nonEmpty: Boolean = synchronized { pending.nonEmpty }
     def get_edits: List[Text.Edit] = synchronized { pending.toList }
-    def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective }
-    def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit =
+    def get_last_perspective: Document.Node.Perspective_Text.T = synchronized { last_perspective }
+    def set_last_perspective(perspective: Document.Node.Perspective_Text.T): Unit =
       synchronized { last_perspective = perspective }
 
     def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
@@ -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)
   }
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -53,6 +53,17 @@
     } yield doc_view.model.node_name).contains(name)
 
 
+  /* global changes */
+
+  def state_changed(): Unit = {
+    GUI_Thread.later { flush() }
+    PIDE.plugin.deps_changed()
+    session.global_options.post(Session.Global_Options(PIDE.options.value))
+  }
+
+  override def document_state_changed(): Unit = state_changed()
+
+
   /* current situation */
 
   override def current_node(view: View): Option[Document.Node.Name] =
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -86,23 +86,23 @@
   val spell_checker = new Spell_Checker_Variable
 
 
-  /* global changes */
-
-  def options_changed(): Unit = {
-    session.global_options.post(Session.Global_Options(options.value))
-    delay_load.invoke()
-  }
-
-  def deps_changed(): Unit = {
-    delay_load.invoke()
-  }
-
-
   /* theory files */
 
-  lazy val delay_init: Delay =
+  private lazy val delay_init: Delay =
     Delay.last(PIDE.session.load_delay, gui = true) { init_models() }
 
+  private lazy val delay_load: Delay =
+    Delay.last(session.load_delay, gui = true) {
+      if (JEdit_Options.continuous_checking()) {
+        if (!PerspectiveManager.isPerspectiveEnabled ||
+            JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
+        else if (delay_load_activated()) delay_load_body()
+        else delay_load.invoke()
+      }
+    }
+
+  def deps_changed(): Unit = delay_load.invoke()
+
   private val delay_load_active = Synchronized(false)
   private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
   private def delay_load_activated(): Boolean =
@@ -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) {
@@ -148,16 +150,6 @@
     else delay_load_finished()
   }
 
-  private lazy val delay_load: Delay =
-    Delay.last(session.load_delay, gui = true) {
-      if (JEdit_Options.continuous_checking()) {
-        if (!PerspectiveManager.isPerspectiveEnabled ||
-            JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
-        else if (delay_load_activated()) delay_load_body()
-        else delay_load.invoke()
-      }
-    }
-
   private def file_watcher_action(changed: Set[JFile]): Unit =
     if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
 
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -48,8 +48,8 @@
 
   /* main */
 
-  val status = new Theories_Status(view)
-  set_content(new ScrollPane(status.gui))
+  private val theories = new Theories_Status(view)
+  set_content(new ScrollPane(theories.gui))
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
@@ -60,11 +60,11 @@
         GUI_Thread.later {
           continuous_checking.load()
           logic.load()
-          status.reinit()
+          theories.refresh()
         }
 
       case changed: Session.Commands_Changed =>
-        GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) }
+        GUI_Thread.later { theories.update(domain = Some(changed.nodes), trim = changed.assignment) }
     }
 
   override def init(): Unit = {
@@ -73,7 +73,7 @@
     PIDE.session.commands_changed += main
 
     handle_phase(PIDE.session.phase)
-    status.update()
+    theories.update()
   }
 
   override def exit(): Unit = {
diff -r c48fe2be847f -r 5364cdc3ec0e src/Tools/jEdit/src/theories_status.scala
--- a/src/Tools/jEdit/src/theories_status.scala	Tue Dec 20 18:20:19 2022 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala	Tue Dec 20 19:43:55 2022 +0100
@@ -24,8 +24,18 @@
   /* component state -- owned by GUI thread */
 
   private var nodes_status = Document_Status.Nodes_Status.empty
-  private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
-  private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
+  private var nodes_required = Set.empty[Document.Node.Name]
+  private var document_required = Set.empty[Document.Node.Name]
+
+  private def init_state(): Unit = GUI_Thread.require {
+    if (document) {
+      nodes_required = PIDE.editor.document_required().toSet
+    }
+    else {
+      nodes_required = Document_Model.nodes_required()
+      document_required = PIDE.editor.document_required().toSet
+    }
+  }
 
 
   /* node renderer */
@@ -51,6 +61,9 @@
   }
 
   private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+    private val document_marker = Symbol.decode(" \\<^file>")
+    private val no_document_marker = "   "
+
     private object component extends BorderPanel {
       opaque = true
       border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
@@ -143,10 +156,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
+      component.label.text =
+        name.theory_base_name +
+        (if (document_required.contains(name)) document_marker else no_document_marker)
       component
     }
   }
@@ -172,7 +186,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)
@@ -203,7 +219,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()
@@ -213,23 +233,27 @@
         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(PIDE.editor.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
+        }
     }
   }
 
 
-  /* reinit */
+  /* refresh */
 
-  def reinit(): Unit = {
-    GUI_Thread.require {}
-
-    theory_required = Document_Model.required_nodes(false)
-    document_required = Document_Model.required_nodes(true)
+  def refresh(): Unit = GUI_Thread.require {
+    init_state()
     gui.repaint()
   }
+
+  init_state()
 }