Re: [isabelle] RC1: Immediate completion on \-symbols

On Fri, 22 Jan 2016, Peter Lammich wrote:

However, if you type a backslash in Isabelle, you almost always want a completion. The new behaviour makes it just more typing to get it.

This is not true. Try typing some Isabelle document text, with a mixture of Isabelle symbols and LaTeX macros. That was impossible before, and is now quite convenient.

I have already mentioned the new etc/abbrevs a few times. It provides a lot of freedom to invent private abbreviations. For example, you could use "#a" = "\<alpha>" etc. You merely need to figure out a non-letter character that is not used elsewhere in important combinations.


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