Re: [isabelle] jEdit: Abbreviations



On 2/14/2013 8:45 AM, Peter Lammich wrote:

... But this leaves the "<" in place for me, and I end up with
  "'<\<gamma>" in the buffer.

I really would like some escape-character that brings up the completions
even inside words, optimally with automatic replacement as I'm used from
PG.

I jumped to conclusions and didn't actually hit the tab key to do the completion, so that's the way it works for me also.

The key sequence "\<" is an escape-key-sequence. The bad thing about it is that both characters use the right hand, and one of them uses the shift key.

If you had an escape character, you would save pressing two keys if it didn't use the shift key, and save only pressing one key if it used the shift key.

As far as automatic replacement, I don't know about that.

Regards,
GB





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