--- 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)"
--- 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
--- 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")
--- 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("<html><b>Build</b></html>") {
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()
+ }
+ }
}
}
}