When using e.g. Lean4-mode, it is often the case that one wants to update the proof state window by moving the cursor without changing the source. This is way less resource intensive than an update to the source. However, setting the update timer to a very small value causes high CPU load when actually editing the file.
Solution: Split timer into read-only timer and write timer. When the buffer content is not edited, the read-only timer is activated to achieve better update times. Otherwise, the write timer is activated.