Re: [isabelle] Proof General 4+emacs 23.2: delete-selection-mode
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 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
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.
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
This archive was generated by a fusion of
Pipermail (Mailman edition) and