# HG changeset patch
# User wenzelm
# Date 1665940347 -7200
# Node ID 085b37d13d411b628ae12f6d2afed3a8c18e47e0
# Parent  4556f76d216eebc3d883cf40fac11e44c6422734
tuned signature;

diff -r 4556f76d216e -r 085b37d13d41 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Oct 16 16:09:33 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Oct 16 19:12:27 2022 +0200
@@ -134,12 +134,11 @@
     ) {
       def nodes_status_update(state: Document.State, version: Document.Version,
         domain: Option[Set[Document.Node.Name]] = None,
-        trim: Boolean = false,
-        tick: Boolean = false
+        trim: Boolean = false
       ): (Boolean, Use_Theories_State) = {
         val (nodes_status_changed, nodes_status1) =
           nodes_status.update(resources, state, version, domain = domain, trim = trim)
-        val st1 = copy(last_update = if (tick) Time.now() else last_update, nodes_status = nodes_status1)
+        val st1 = copy(last_update = Time.now(), nodes_status = nodes_status1)
         (nodes_status_changed, st1)
       }
 
@@ -346,7 +345,7 @@
 
                   val (nodes_status_changed, st1) =
                     st.nodes_status_update(state, version,
-                      domain = Some(domain), trim = changed.assignment, tick = true)
+                      domain = Some(domain), trim = changed.assignment)
 
                   if (nodes_status_delay >= Time.zero && nodes_status_changed) {
                     delay_nodes_status.invoke()