removed obsolete parameter (see 7c23db6b857b);
authorwenzelm
Tue, 31 Jan 2023 14:32:07 +0100
changeset 77145 de618831ffd9
parent 77144 42c3970e1ac1
child 77146 eb114301c4df
removed obsolete parameter (see 7c23db6b857b);
src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 12:27:00 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 14:32:07 2023 +0100
@@ -150,7 +150,7 @@
   private def finish_process(output: XML.Body): Unit =
     current_state.change(_.finish(output))
 
-  private def run_process(only_running: Boolean = false)(body: Log_Progress => Unit): Boolean = {
+  private def run_process(body: Log_Progress => Unit): Boolean = {
     val started =
       current_state.change_result { st =>
         if (st.process.is_finished) {
@@ -171,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(
@@ -225,7 +225,7 @@
     if (document_session.is_vacuous) true
     else if (document_session.is_pending) false
     else {
-      run_process(only_running = true) { progress =>
+      run_process { progress =>
         show_page(output_page)
         val result = Exn.capture { document_build(document_session, progress) }
         val msgs =