# HG changeset patch # User wenzelm # Date 1675180833 -3600 # Node ID 3991a35cd7402331373b02beaa81ce429e8a8e84 # Parent 9b3a8565464d479c7c43b3d57b362b863ed98ff3 automatically build document when selected theories are finished; diff -r 9b3a8565464d -r 3991a35cd740 etc/options --- a/etc/options Tue Jan 31 16:13:27 2023 +0100 +++ b/etc/options Tue Jan 31 17:00:33 2023 +0100 @@ -225,6 +225,12 @@ public option editor_document_session : string = "" -- "session for interactive document preparation" +public option editor_document_auto : bool = false + -- "automatically build document when selected theories are finished" + +public option editor_document_delay : real = 2.0 + -- "delay for document auto build" + option editor_execution_delay : real = 0.02 -- "delay for start of execution process after document update (seconds)" diff -r 9b3a8565464d -r 3991a35cd740 src/Pure/PIDE/document_editor.scala --- a/src/Pure/PIDE/document_editor.scala Tue Jan 31 16:13:27 2023 +0100 +++ b/src/Pure/PIDE/document_editor.scala Tue Jan 31 17:00:33 2023 +0100 @@ -29,6 +29,7 @@ ) { def is_vacuous: Boolean = background.isEmpty def is_pending: Boolean = snapshot.isEmpty + def is_ready: Boolean = background.isDefined && snapshot.isDefined def get_background: Sessions.Background = background.get def get_variant: Document_Build.Document_Variant = get_background.info.documents.head diff -r 9b3a8565464d -r 3991a35cd740 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Tue Jan 31 16:13:27 2023 +0100 +++ b/src/Pure/PIDE/session.scala Tue Jan 31 17:00:33 2023 +0100 @@ -147,6 +147,7 @@ def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def update_delay: Time = session_options.seconds("editor_update_delay") + def document_delay: Time = session_options.seconds("editor_document_delay") def chart_delay: Time = session_options.seconds("editor_chart_delay") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") diff -r 9b3a8565464d -r 3991a35cd740 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 16:13:27 2023 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Tue Jan 31 17:00:33 2023 +0100 @@ -141,12 +141,19 @@ private def pending_process(): Unit = current_state.change { st => if (st.pending) st - else { delay_build.invoke(); st.copy(pending = true) } + else { + delay_auto_build.revoke() + delay_build.invoke() + st.copy(pending = true) + } } private def finish_process(output: XML.Body): Unit = current_state.change { st => - if (st.pending) delay_build.invoke() + if (st.pending) { + delay_auto_build.revoke() + delay_build.invoke() + } st.finish(output) } @@ -254,6 +261,16 @@ if (!document_build_attempt()) delay_build.invoke() } + private lazy val delay_auto_build: Delay = + Delay.last(PIDE.session.document_delay, gui = true) { + pending_process() + } + + private def document_pending() = current_state.value.pending + + private val document_auto = new JEdit_Options.Bool_Access("editor_document_auto") + + /* controls */ @@ -275,6 +292,15 @@ override def clicked(): Unit = PIDE.editor.document_select_all(set = true) } + private val auto_build_button = + new JEdit_Options.Bool_GUI(document_auto, "Auto") { + tooltip = Word.capitalize(document_auto.description) + override def clicked(state: Boolean): Unit = { + super.clicked(state) + if (state) delay_auto_build.invoke() + } + } + private val build_button = new GUI.Button("Build") { tooltip = "Build document" @@ -295,7 +321,7 @@ private val controls = Wrap_Panel(List(document_session, process_indicator.component, load_button, - build_button, view_button, cancel_button)) + auto_build_button, build_button, view_button, cancel_button)) add(controls.peer, BorderLayout.NORTH) @@ -360,9 +386,20 @@ 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 (current_state.value.pending) delay_build.invoke() + if (domain.nonEmpty) theories.update(domain = Some(domain)) + + val pending = document_pending() + val auto = document_auto() + if (changed.assignment || domain.nonEmpty || pending || auto) { + if (PIDE.editor.document_session().is_ready) { + if (pending) { + delay_auto_build.revoke() + delay_build.invoke() + } + else if (auto) { + delay_auto_build.invoke() + } + } } } }