# HG changeset patch
# User wenzelm
# Date 1671558197 -3600
# Node ID 3f50b24909dfae4726d2f77fed911aae5f14b471
# Parent  4db6852313269edf7d463beafe8704b1fe16c345
clarified process management;

diff -r 4db685231326 -r 3f50b24909df src/Tools/jEdit/src/document_dockable.scala
--- 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 =