Re: [isabelle] jEdit: Abbreviations

On Thu, 14 Feb 2013, Makarius wrote:

Since the application is just for a few exceptional cases, you can try to use the on-board Abbreviation mechanism

Maybe it was not clear that this refers to the built-in mechanism that is configure via "Global Options / Abbreviations". It also has its own rules about "word" boundaries for completions that need to be explored. There are separate keyboard actions to activate replacement.


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