# 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 } }) }