--- a/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 18:33:51 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 20 18:43:17 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)
}
}
@@ -124,86 +122,90 @@
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 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_setup(Some(session_background))
+ 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))
- 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) }
- }
+ finish_process(Nil)
+ 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) =>
+ 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.print(exn))
- }
- current_state.change(_.finish(msg))
- process_finished()
+ 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_state()
+ show_state()
- 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_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
+ GUI_Thread.later { progress.load() }
}
- show_state()
}
@@ -230,7 +232,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 =