clarified GUI events;

--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 19:50:58 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 20:09:03 2023 +0100
@@ -301,7 +301,9 @@
       tooltip = Word.capitalize(document_auto.description)
       override def clicked(state: Boolean): Unit = {
         super.clicked(state)
+
         if (state) delay_auto_build.invoke()
+        else delay_auto_build.revoke()
       }
     }