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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
