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