tuned signature;
authorwenzelm
Tue, 06 Dec 2022 18:37:57 +0100
changeset 76584 017384868fcb
parent 76583 c9f897077089
child 76585 1b7bb4f8c0f4
tuned signature;
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()
       }
     }
   }