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 option.

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

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 MHonArc.