Email Gateway (Dec 03 2025 at 08:28): Email Gateway (Dec 03 2025 at 08:28):From: Ian Hayes <cl-isabelle-users@lists.cam.ac.uk>
Hi Makarius,
An issue I've been having for a few releases is that if I delete a range
of complete lines in the JEdit IDE, it non-deterministically goes into a
strange state where after deletion a range of lines corresponding to the
position on the screen where the deleted lines were, is selected, with
the cursor at the end. By whole lines I mean the selected range is a
sequence of whole lines with the cursor at the start of the following
line. If I select the same lines but have the cursor at the end of the
last line, the issue does not occur.
On top of that also non-deterministically, after it gets in that strange
state, I may or may not be able to move the cursor using cursor keys -
more precisely I move the cursor and it immediately moves it back. And
on top of that it can get into a very weird state where the cursor
autonomously moves around and selects text and may paste in selected
text at the cursor, like is generating its own input events out of
nowhere. For these latter issues I just have to re-start Isabelle.
I have got into the habit of never deleting a range of whole lines, so
the problem has simple work around.
Perhaps you could look into this for the next release.
I'm running the latest version of MacOS on a Mac Mini M4 Pro.
Best regards
Ian
On 20/2/2025 01:00, Makarius wrote:
Dear Isabelle users,
the release train for Isabelle2025 (March 2025) has arrived at the
station Isabelle2025-RC3, see again
https://isabelle-dev.sketis.net/phame/post/view/85/release_candidates_for_isabelle2025The website is https://isabelle.in.tum.de/website-Isabelle2025-RC3
with the usual downloads for Linux (Intel), Linux (ARM), macOS (Intel
and ARM), Windows (Intel).This release candidate is sufficiently finished to be ready for
applications. There will be 3 more weeks until everything becomes
unchangeable, until the next release in 8-10 months.Any feedback about Isabelle release candidates should be posted with a
meaningful Subject, not just a clone of the announcement.Makarius
Last updated: Dec 21 2025 at 20:24 UTC