Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proof General 4+emacs 23.2: delete-selection-mode

view this post on Zulip Email Gateway (Aug 18 2022 at 17:03):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hello,
I'm experiencing problems with delete-selection-mode in the PG version
shipped with the 2011-release of Isabelle.
I'm using emacs 23.2.1.

delete-selection-mode simply does not work, i.e. hitting the <delete>
key does not delete the selection, independent of the state of the
delete-selection-mode option.
When starting emacs without proof general, everything works fine.

Has anyone a similar problem. Do you know a workaround?

Best,
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 17:03):

From: David Aspinall <David.Aspinall@ed.ac.uk>
Delete selection mode uses properties on symbols for commands that get
remapped when you have Unicode Tokens switched on (so that, e.g., delete
deletes a symbol in one go even though the actual buffer contents is
several characters).

These lines in .emacs fix delete selection:

(put 'unicode-tokens-delete-backward-char 'delete-selection 'supersede)
(put 'unicode-tokens-delete-char 'delete-selection 'supersede)

Peter verified this off list. This patch will go in to PG 4.1.

- David

Last updated: Apr 27 2024 at 01:05 UTC