Email Gateway (Apr 02 2026 at 17:50): Email Gateway (Apr 02 2026 at 17:50):From: Bartosz Glowacki <cl-isabelle-users@lists.cam.ac.uk>
Dear Isabelle developers,
I found a bug in Delay.run() (src/Pure/Concurrent/delay.scala, line 29) where a non-interrupt exception is logged but then rethrown. The rethrown exception propagates through TimerTask.run() into java.util.TimerThread.mainLoop(), which does not catch RuntimeException from tasks — the timer thread terminates and the global event_timer singleton dies permanently.
After that, every Delay.invoke() call in the process either throws IllegalStateException ("Timer already cancelled") or silently fails. This breaks all debouncing and throttling in the editor.
Call chain:
Delay.invoke() → Event_Timer.request() → TimerTask fires → Delay.run()
→ catch block logs + rethrows → escapes TimerTask.run() → kills TimerThread
Minimal fix — remove the rethrow in delay.scala line 29 (Isabelle2025/src/Pure/Concurrent/delay.scala:29):
Patch is attached to this email.
The exception is still logged for visibility, but Delay.run() exits normally so TimerThread.mainLoop() continues its loop and the global timer stays alive.
I have a standalone test (DelayBugTest) that reproduces this reliably:
The test passes after applying the fix above.
I am aware that there is a known bug that jEdit slows down after a long time. I am not sure, but I believe it might be somehow connected, that there is some runtime exception, which silently kills the timer and the perceived 'slowdown' is just the fact that some tasks that use timer are not executed, however, this requires further tests.
I am happy to provide the full test code or any additional information. This was found as part of my dissertation work on frontend testing of the Isabelle platform.
Best regards,
Bartosz Glowacki
King's College London
Email Gateway (Apr 07 2026 at 18:25):From: Fabian Huch <huch@in.tum.de>
While this does look suspicious, speaking of a 'bug' doesn't really make
sense here: If a task fails with an unrecoverable error on a background
thread, I would expect that the background thread is in a failure state
too. Looking only at your description, I would actually argue that the
system should instead fail immediately (loudly). But judging the
situation requires looking into the sources and history, to find out
what the intention was.
In any case, this is still missing an actual problem -- does the
Exception actually occur, or does the behavior under the hypothesized
state actually coincide with a known issue? If yes, how to trigger the
problem? I have seen this state manifest a couple of times, but only
after a (very obvious) catastrophic failure somewhere else.
Fabian
On 4/2/26 19:24, Bartosz Glowacki (via cl-isabelle-users Mailing List)
wrote:
Dear Isabelle developers,
I found a bug in Delay.run() (src/Pure/Concurrent/delay.scala, line
29) where a non-interrupt exception is logged but then rethrown. The
rethrown exception propagates through TimerTask.run() into
java.util.TimerThread.mainLoop(), which does not catch
RuntimeException from tasks — the timer thread terminates and the
global event_timer singleton dies permanently.After that, every Delay.invoke() call in the process either throws
IllegalStateException ("Timer already cancelled") or silently fails.
This breaks all debouncing and throttling in the editor.Call chain:
Delay.invoke() → Event_Timer.request() → TimerTask fires → Delay.run()
→ catch block logs + rethrows → escapes TimerTask.run() → kills
TimerThreadMinimal fix — remove the rethrow in delay.scala line 29
(Isabelle2025/src/Pure/Concurrent/delay.scala:29):
Patch is attached to this email.The exception is still logged for visibility, but Delay.run() exits
normally so TimerThread.mainLoop() continues its loop and the global
timer stays alive.I have a standalone test (DelayBugTest) that reproduces this reliably:
1. Create a Delay whose event throws RuntimeException
2. Invoke it and wait for it to fire
3. Create a second Delay and try to invoke it
4. The second invoke throws IllegalStateException — the timer is deadThe test passes after applying the fix above.
I am aware that there is a known bug that jEdit slows down after a
long time. I am not sure, but I believe it might be somehow connected,
that there is some runtime exception, which silently kills the timer
and the perceived 'slowdown' is just the fact that some tasks that use
timer are not executed, however, this requires further tests.I am happy to provide the full test code or any additional
information. This was found as part of my dissertation work on
frontend testing of the Isabelle platform.Best regards,
Bartosz Glowacki
King's College London
Last updated: Apr 12 2026 at 02:50 UTC