[isabelle-dev] Sidekick completion in Isabelle/jEdit
makarius at sketis.net
Fri Apr 20 14:29:57 CEST 2012
On Wed, 18 Apr 2012, Christian Sternagel wrote:
> Concerning convenience of input and automatic replacement:
> I would not use automatic replacement at all, since it is at least as
> often a problem as it is of help (e.g., ML code inside theories "=>" in
> case statements, the mentioned "~~/" for imports, and I am sure that
> there are many other examples [LaTeX inside @text blocks]).
I am also a member of the club "explicit is better than implicit". It is a
matter of fine tuning what that means exactly here.
> Still it is very convenient if one can just type and does not have to
> click (or browse with the keyboard) any popups.
> In jEdit you can do the following (see also
I have made some experiments based on these explanations, see
The relevant properties are:
This already makes quite some improvement over the naive earlier defaults,
i.e. it requires 0 or 1 extra keystrokes to get the intended result in
What is interesting is that the GUI focus for the popup does not prevent
from typing regular characters in the text, so even with the convenient
default of true here, it is quite non-intrusive. What I still did not get
is the purpose of \t, since the popup seems to absorb that key without any
Likewise, some other important key sequences are absorbed without any
immediate effect, notably control sequences such as C-d or A-d to delete
things in the text. Maybe that is not intended, and needs some refinement
of Sidekick itself. OO was invented for such patching of existing
implementations, so one could try without patching the Sidekick sources.
I won't start anything like that before the release, though.
More information about the isabelle-dev