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
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
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
As far as automatic replacement, I don't know about that.
This archive was generated by a fusion of
Pipermail (Mailman edition) and