# HG changeset patch
# User wenzelm
# Date 1675171927 -3600
# Node ID de618831ffd9204797d252e32d3de8764b1dec79
# Parent  42c3970e1ac13b94f25c8396540ea2c0cb9b2398
removed obsolete parameter (see 7c23db6b857b);

diff -r 42c3970e1ac1 -r de618831ffd9 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 =