Email Gateway (Nov 19 2025 at 13:15): Email Gateway (Nov 19 2025 at 13:15):From: Ian Hayes <mail@ian-hayes.id.au>
Hi Makarius,
Isabelle2025-1-RC1 exhibits the same issues I was having with using a
mouse on a Mac on Isabelle-2025 (see below for copies of my posts).
These issues make it frustrating to use Isabelle because one often has
to repeat mouse clicks many times before they work. The issues have been
in Isabelle for many years. They are exacerbated when one uses a (higher
resolution) Apple Magic Mouse as compared to the track pad or an old
Dell wheel mouse (although they occur with all three).
From my mailing list post 6/2/2025:
<https://lists.cam.ac.uk/sympa/msg/cl-isabelle-users/2025-02/vsz7n4TvV8DU6LkdrX4hOA>
--
A slight movement of the mouse when Command clicking through to a
lemma/definition means it fails and selects the character under the
cursor. I'm guessing this is something to do with the fact that the
Command click occurs, not on pressing the mouse, but when it is then
released. For example, if you Command press and move the mouse a little
and then release, it won't go through to the definition but rather
selects the text under the cursor. And the behaviour is worse when I use
an Apple magic mouse in place of an old mouse -- I suspect because the
Magic mouse will generate a small movement more easily.
A similar issue occurs when clicking on a the output of sledgehammer to
get it to copy the suggested proof into the theory file.
Another issue is double-clicking the name of a theory in the theories
menu is also flaky if the mouse moves slightly between the two clicks,
even if one remains within the same menu item.
--
From my mailing list post 10/2/2025
<https://lists.cam.ac.uk/sympa/msg/cl-isabelle-users/2025-02/EG0nW0_Z5p704b34yHE6eA>
--
For MacOS for a left mouse click there are the following mouse events:
* Press down the button: NSLeftMouseDown which invokes mouseDown
* Move the mouse while pressing the button: NSLeftMouseDragged which
invokes mouseDragged
* Release the button:|NSLeftMouseUp which invokesmouseUp|
* ||Move the mouse without pressing any button: NSMouseMoved which
invokes mouseMoved
A combination of mouseDown-mouseDragged-mouseUp selects the text between
the coordinates of the mouseDown and mouseUp. The problem with
Command-click would appear to be that the text selection behaviour is
happening when the Command key is held down (for a click through) and
the selection behaviour is taking precedence over the Command click*. If
the selection behaviour was disabled while the Command key is held down
that might fix the problem. Alternatively, the Command click behaviour
should take precedence over selection of text.
*In practice, sometimes it recognises the Command-click and other it
recognises a selection, so this looks like a classic (concurrency) race
between the two actions. With the Command key held down, mouseDown-move
a few characters-mouseUp always selects the text, even if it is in the
one name.
An alternative scenario is the following.
The mouseDown-mouseUp combination (*without *Command key held) moves the
cursor to the location of the mouse. With the Command key held down, it
non-deterministically either moves the cursor or clicks through to the
definition. Again this looks like a race between the two actions. If the
cursor movement action was disabled while the Command key is held down
or the Command-click given precedence that may work.
From my experimentation, it appears the Command-click does not happen
until the mouse is released (mouseUp). If the Command click action was
invoked on mouseDown, the issue might be resolved.
Using the track-pad rather than the mouse is more reliable but can still
exhibit the same behaviour. The detailed behaviour is that with Command
held down, mouseDown moves the cursor to the mouse location and on
mouseUp it moves it to the definition of the item. On some occasions it
just moves the cursor to the mouse location and does not go to the
definition, and on other occasions it moves the cursor to the mouse
position and removes the highlight from the item under the mouse, where
by highlight, I mean the highlighting that occurs when one presses the
Command key.
Another symptom is that if the cursor is on name and the Command key
held, the name is not highlighted, but if one leaves the Command key
held and moves the cursor a little, the name is then highlighted.
A related symptom is that when the Command key is held and the name
highlighted for a couple of seconds, a pop-up window appears and the
highlight is removed from the name until one moves the cursor again.
An old (lower resolution) Dell wheel mouse is more reliable than the
track-pad, which is in turn more reliable than a magic mouse. But note
that even with the old Dell mouse a small mouse movement between down
and up gives a cursor move or select text action, and not a
click-through to definition action. The symptoms occur on both my old M1
laptop and a new mini with a fresh install of everything.
Probably not relevant here but in the Finder under MacOS, if wants to
select multiple files, one holds down the Command key while clicking on
each file.
Disclaimer: I'm not a mouse event handling expert.
--
Thanks in advance
Ian
On 6/11/2025 04:36, Makarius wrote:
Dear Isabelle users,
this calendar year has two Isabelle releases (which happen every 8-10
months). We are now ready to start the release process for
Isabelle2025-1 (December 2025). See also the continuously updated blog
post https://sketis.net/2025/release-candidates-for-isabelle2025-1The current release candidate is available from
https://isabelle.in.tum.de/website-Isabelle2025-1-RC1A corresponding version of the Archive of Formal Proofs is
https://isabelle.sketis.net/repos/afp-devel/rev/695d78dfa92aThe NEWS and ANNOUNCE files are already up-to-date, but some
documentation still requires update.The coming weeks are dedicated to thorough testing of release
candidates. Afterwards the release will become final and unchangeable
as usual.Any feedback about Isabelle release candidates should be posted with a
meaningful Mail subject, not just a clone of this announcement.Makarius
Email Gateway (Nov 23 2025 at 15:37):From: Makarius <makarius@sketis.net>
On 17/11/2025 02:03, Ian Hayes wrote:
Isabelle2025-1-RC1 exhibits the same issues I was having with using a mouse on
a Mac on Isabelle-2025 (see below for copies of my posts). These issues make
it frustrating to use Isabelle because one often has to repeat mouse clicks
many times before they work. The issues have been in Isabelle for many years.
They are exacerbated when one uses a (higher resolution) Apple Magic Mouse as
compared to the track pad or an old Dell wheel mouse (although they occur with
all three).
Hi Ian,
a few days ago, I was about to dig up the old mail thread, to point out that
RC2 has addresses most of these problems. The main idea is to use
"MousePressed" events instead of "MouseClicked". The latter requires to
release the button to be "committed", but the Magic Mouse does not like that.
This already makes a big difference, but now another problem shows up: When
following hyperlinks via C-hover-click, there is often a selection range
showing up on the target buffer. Maybe I find a solution for that until RC3
(presumably published next Wednesday).
Generally note that the time to sort out old problems (that are not
regressions from the previous release) is before the release process starts
with RC1: RC0 is a good event to take as a reminder.
Makarius
Email Gateway (Dec 01 2025 at 15:51):From: Makarius <makarius@sketis.net>
On 23/11/2025 16:36, Makarius wrote:
RC2 has addresses most of these problems. The main idea is to use
"MousePressed" events instead of "MouseClicked". The latter requires to
release the button to be "committed", but the Magic Mouse does not like that.This already makes a big difference, but now another problem shows up: When
following hyperlinks via C-hover-click, there is often a selection range
showing up on the target buffer. Maybe I find a solution for that until RC3
(presumably published next Wednesday).
RC3 was delayed several days, but it should now work properly. We have a new
mouse handler, specifically for Isabelle/jEdit -- based on the regular mouse
handler from jEdit.
That requires serious testing by everybody, especially on macOS, but the
handler is uniform for all platforms.
Makarius
Last updated: Dec 02 2025 at 16:32 UTC