clarified guard: avoid spurious auto builds;
authorwenzelm
Tue, 31 Jan 2023 17:04:02 +0100
changeset 77150 286fdf0fcc44
parent 77149 3991a35cd740
child 77151 2f43be96c713
clarified guard: avoid spurious auto builds;
src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:00:33 2023 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Tue Jan 31 17:04:02 2023 +0100
@@ -386,12 +386,12 @@
       case changed: Session.Commands_Changed =>
         GUI_Thread.later {
           val domain = PIDE.editor.document_theories().filter(changed.nodes).toSet
-          if (domain.nonEmpty) theories.update(domain = Some(domain))
+          if (domain.nonEmpty) {
+            theories.update(domain = Some(domain))
 
-          val pending = document_pending()
-          val auto = document_auto()
-          if (changed.assignment || domain.nonEmpty || pending || auto) {
-            if (PIDE.editor.document_session().is_ready) {
+            val pending = document_pending()
+            val auto = document_auto()
+            if ((pending || auto) && PIDE.editor.document_session().is_ready) {
               if (pending) {
                 delay_auto_build.revoke()
                 delay_build.invoke()