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
Von: Makarius
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 MHonArc.