Re: [isabelle] Isabelle2008



> You canre-bind keys to x-symbol-copy-region-encoded and
> x-symbol-yank-decoded, but I haven't found an equivalent for cut (kill
> in xemacs speak, I guess) and it wasn't painful enough yet to write one.
> 
> (global-set-key [(meta c)] 'x-symbol-copy-region-encoded)
> (global-set-key [(meta v)] 'x-symbol-yank-decoded)

Thanks, I didn't know these exist.

On Aquamacs: copy/paste works fine here, but is screwed up by PG: once
PG is loaded, you can no longer cut/paste reliably between the editor
and the outside world :-(

Tobias





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.