Email Gateway (Dec 05 2025 at 11:45): Email Gateway (Dec 05 2025 at 11:45):From: Lawrence Paulson via isabelle-dev <isabelle-dev@mailman.proof.cit.tum.de>
An issue I sometimes get to (certainly with the current release) is a mouse selection sticking at one end. No matter how you click the mouse, it seems to think you are trying to extend a selection rather than move the cursor. The same thing happened if you tried to move it with the cursor keys. Eventually it starts pasting things and the result is chaos. Then you simply have to quit. It happened a couple of days ago and I recorded a brief movie of it, see the link.
Larry
Last updated: Dec 10 2025 at 12:50 UTC