# HG changeset patch # User wenzelm # Date 1671550453 -3600 # Node ID a7602257a8257340c3dbe79561f743136648a256 # Parent bf5ff407f32f4cb98e9947795419f31f16013e7d clarified state document nodes for Theories_Status / Document_Dockable; diff -r bf5ff407f32f -r a7602257a825 src/Pure/PIDE/document_editor.scala --- 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, diff -r bf5ff407f32f -r a7602257a825 src/Pure/PIDE/document_status.scala --- 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 { diff -r bf5ff407f32f -r a7602257a825 src/Pure/PIDE/editor.scala --- 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)) diff -r bf5ff407f32f -r a7602257a825 src/Pure/PIDE/headless.scala --- 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 diff -r bf5ff407f32f -r a7602257a825 src/Pure/Tools/server.scala --- 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)) } diff -r bf5ff407f32f -r a7602257a825 src/Tools/VSCode/src/vscode_resources.scala --- 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 = diff -r bf5ff407f32f -r a7602257a825 src/Tools/jEdit/src/document_dockable.scala --- 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() } diff -r bf5ff407f32f -r a7602257a825 src/Tools/jEdit/src/main_plugin.scala --- 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) { diff -r bf5ff407f32f -r a7602257a825 src/Tools/jEdit/src/theories_status.scala --- 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 + } } }