[isabelle-dev] Sidekick completion in Isabelle/jEdit

[Makarius]

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 
> https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2011-November/msg00089.html

I have made some experiments based on these explanations, see 
Isabelle/8bdfacbc2fa2

The relevant properties are:

sidekick.auto-complete-popup-get-focus=true
sidekick.complete-instant.toggle=false
sidekick.complete-popup.accept-characters=\\n\\t
sidekick.complete-popup.insert-characters=

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 
most situations.

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 
effect.

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.


 	Makarius