Stream: Mirror: Isabelle Development Mailing List

Topic: NEWS: Isabelle/jEdit: more robust and reactive mouse hand...

Email Gateway (Dec 01 2025 at 16:47):

From: Makarius <makarius@sketis.net>

* Isabelle/jEdit Prover IDE *

• Mouse event handling is now more robust and more reactive: this is
  especially relevant for macOS with Magic Mouse. The mouse reacts on
  pressing the button, and does not wait for its release. After jumping
  around in the editor, e.g. when following hyperlinks, mouse drag events
  are ignored (according to system option "editor_jump_delay", with
  default 0.3 seconds): this avoids spurious text selection after editor
  navigation.

This refers to Isabelle/763ff9c96be2, which is from Isabelle-2025-1-RC3, but
now back on isabelle-dev. It is a refinement of earlier attempts on mouse
handling that did not work out properly.

It is important to keep an eye on mouse handling within the next 2 weeks. If
there is anything seriously wrong, it needs to be addressed for the
Isabelle2025-1 release, before that becomes final.

Makarius

Email Gateway (Dec 02 2025 at 11:15):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

I have tried the new mouse handling with a magic mouse and I'd like it much, much more than the previous behaviour.

This remind me of another mouse-related problem, intermittent unfortunately, but I think connected with typing/pasting over the current selection: it gets into a crazy state where it thinks the cursor position as one half of a selection and interprets any other mouse click as the other half. Generally, it goes berserk after this and often there's no alternative to closing the window or even quitting altogether, as sometimes it starts pasting and making an unrecoverable mess of your proof. Maybe this is just part of the magic of a magic mouse.

• Mouse event handling is now more robust and more reactive: this is
  especially relevant for macOS with Magic Mouse. The mouse reacts on
  pressing the button, and does not wait for its release. After jumping
  around in the editor, e.g. when following hyperlinks, mouse drag events
  are ignored (according to system option "editor_jump_delay", with
  default 0.3 seconds): this avoids spurious text selection after editor
  navigation.

Email Gateway (Dec 02 2025 at 12:53):

From: Makarius <makarius@sketis.net>

On 02/12/2025 12:15, Lawrence Paulson wrote:

This remind me of another mouse-related problem, intermittent unfortunately,
but I think connected with typing/pasting over the current selection: it gets
into a crazy state where it thinks the cursor position as one half of a
selection and interprets any other mouse click as the other half. Generally,
it goes berserk after this and often there's no alternative to closing the
window or even quitting altogether, as sometimes it starts pasting and making
an unrecoverable mess of your proof. Maybe this is just part of the magic of a
magic mouse.

There is a > 0 chance that the new mouse handler prevents that.

If it still happens again, can you make a screen recording on macOS and show
it to me?

Makarius

Email Gateway (Dec 02 2025 at 15:21):

From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>

Believe it or not, it happened just today (only with the current release). Possibly running for a long time and exhausting memory could be related. What you see here is my repeated mouse clicking, trying to clear the previous selection, but jEdit will not let go. Eventually it starts moving text and pasting wildly.

If it still happens again, can you make a screen recording on macOS and show
it to me?

Makarius

jedit mouse issue.mp4

Last updated: Dec 10 2025 at 12:50 UTC