Re: [isabelle] RC1: Immediate completion on \-symbols
Ok, I never tried that with the jedit based ide.
However, the main purpose of the ide is creating Isabelle proof text, being a convenient latex editor is a nice add on.
Although I would be much more happy with the old behaviour, I will get used to the new one, the additional typing overhead is not that bad at all, so its probably not worth discussing this further.
In general, whenever you do a non backward compatible change in the user interface, you are likely to annoy some of the power users, on which you force a new interfacing mode instead of letting them choose which they like more.
-------- Originalnachricht --------
Betreff: Re: [isabelle] RC1: Immediate completion on \-symbols
An: Peter Lammich
Cc: "C. Diekmann" ,isabelle-users
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" = "\" 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