# HG changeset patch
# User wenzelm
# Date 1534667542 -7200
# Node ID 7e1978b9a4d1bbe3b9aac01d2b54150082d4eb09
# Parent  add44e2b8cb0514c61e11f84d595c2aed548fbbe
suppress redundant messages;

diff -r add44e2b8cb0 -r 7e1978b9a4d1 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Aug 18 22:09:09 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sun Aug 19 10:32:22 2018 +0200
@@ -162,17 +162,15 @@
 
               if (nodes_status_delay >= Time.zero) {
                 nodes_status_update.change(
-                  { case (nodes_status, names) =>
+                  { case upd @ (nodes_status, _) =>
                       val domain =
                         if (nodes_status.is_empty) dep_theories_set
                         else changed.nodes.iterator.filter(dep_theories_set).toSet
-                      val update =
+                      val upd1 =
                         nodes_status.update(resources.session_base, state, version,
-                          domain = Some(domain), trim = changed.assignment)
-                      update match {
-                        case None => (nodes_status, names)
-                        case Some(upd) => delay_nodes_status.invoke; upd
-                      }
+                          domain = Some(domain), trim = changed.assignment).getOrElse(upd)
+                      if (upd == upd1) upd
+                      else { delay_nodes_status.invoke; upd1 }
                   })
               }