# HG changeset patch
# User wenzelm
# Date 1670348277 -3600
# Node ID 017384868fcb152550febc7b1be9cd818bcfe695
# Parent  c9f89707708993494100e4b427f6e0fd12aee5a9
tuned signature;

diff -r c9f897077089 -r 017384868fcb src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 06 16:52:35 2022 +0100
+++ b/src/Tools/jEdit/src/main_plugin.scala	Tue Dec 06 18:37:57 2022 +0100
@@ -106,8 +106,10 @@
     }
 
   private val delay_load_active = Synchronized(false)
+  private def delay_load_finished(): Unit = delay_load_active.change(_ => false)
   private def delay_load_activated(): Boolean =
     delay_load_active.guarded_access(a => Some((!a, true)))
+
   private def delay_load_action(): Unit = {
     if (JEdit_Options.continuous_checking() && delay_load_activated() &&
         PerspectiveManager.isPerspectiveEnabled) {
@@ -156,13 +158,13 @@
                   Document_Model.provide_files(session, loaded_files)
                   delay_init.invoke()
                 }
-                finally { delay_load_active.change(_ => false) }
+                finally { delay_load_finished() }
               }
             }
           }
-          catch { case _: Throwable => delay_load_active.change(_ => false) }
+          catch { case _: Throwable => delay_load_finished() }
         }
-        else delay_load_active.change(_ => false)
+        else delay_load_finished()
       }
     }
   }