# HG changeset patch # User wenzelm # Date 1675173559 -3600 # Node ID 38077c938d01e2c0eaf69fbec222ccead882b42a # Parent eb114301c4dfa46f42ade080a844e977ead54bee defer build until document nodes are ready; diff -r eb114301c4df -r 38077c938d01 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Tue Jan 31 14:37:40 2023 +0100 +++ b/src/Pure/PIDE/document.scala Tue Jan 31 14:59:19 2023 +0100 @@ -589,6 +589,9 @@ def node_files: List[Node.Name] = node_name :: node.load_commands.flatMap(_.blobs_names) + def document_ready(name: Node.Name): Boolean = + state.node_consolidated(version, name) + /* pending edits */ diff -r eb114301c4df -r 38077c938d01 src/Pure/PIDE/document_editor.scala --- a/src/Pure/PIDE/document_editor.scala Tue Jan 31 14:37:40 2023 +0100 +++ b/src/Pure/PIDE/document_editor.scala Tue Jan 31 14:59:19 2023 +0100 @@ -73,7 +73,8 @@ if (background.isEmpty) None else { val snapshot = get_snapshot() - if (snapshot.is_outdated) None else Some(snapshot) + if (snapshot.is_outdated || !selection.forall(snapshot.document_ready)) None + else Some(snapshot) } Session(background, selection, snapshot) } diff -r eb114301c4df -r 38077c938d01 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 14:37:40 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 14:59:19 2023 +0100 @@ -35,8 +35,8 @@ ) { def running: Boolean = !process.is_finished - def run(process: Future[Unit], progress: Progress): State = - copy(process = process, progress = progress) + def run(process: Future[Unit], progress: Progress, reset_pending: Boolean): State = + copy(process = process, progress = progress, pending = if (reset_pending) false else pending) def output(results: Command.Results, body: XML.Body): State = copy(output_results = results, output_main = body) @@ -138,10 +138,19 @@ current_state.change(_.output(results, body)) } + private def pending_process(): Unit = + current_state.change { st => + if (st.pending) st + else { delay_build.invoke(); st.copy(pending = true) } + } + private def finish_process(output: XML.Body): Unit = - current_state.change(_.finish(output)) + current_state.change { st => + if (st.pending) delay_build.invoke() + st.finish(output) + } - private def run_process(body: Log_Progress => Unit): Boolean = { + private def run_process(reset_pending: Boolean = false)(body: Log_Progress => Unit): Boolean = { val started = current_state.change_result { st => if (st.process.is_finished) { @@ -152,7 +161,7 @@ await_process() body(progress) } - (true, st.run(process, progress)) + (true, st.run(process, progress, reset_pending)) } else (false, st) } @@ -162,7 +171,7 @@ private def load_document(session: String): Boolean = { val options = PIDE.options.value - run_process { _ => + run_process() { _ => try { val session_background = Document_Build.session_background( @@ -216,7 +225,7 @@ if (document_session.is_vacuous) true else if (document_session.is_pending) false else { - run_process { progress => + run_process(reset_pending = true) { progress => show_page(output_page) val result = Exn.capture { document_build(document_session, progress) } val msgs = @@ -269,7 +278,7 @@ private val build_button = new GUI.Button("Build") { tooltip = "Build document" - override def clicked(): Unit = delay_build.invoke() + override def clicked(): Unit = pending_process() } private val cancel_button = @@ -351,7 +360,10 @@ case changed: Session.Commands_Changed => GUI_Thread.later { val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet - if (domain.nonEmpty) theories.update(domain = Some(domain)) + if (domain.nonEmpty) { + theories.update(domain = Some(domain)) + if (current_state.value.pending) delay_build.invoke() + } } }