On Sat, 21 Apr 2012, Christian Sternagel wrote:
You should be able to use all characters in accept-characters to finish
the completion. I've just \t in there (not \n) and it works fine for me.
I removed \n, as this completes ":" to \<in> at the end of a line (like
in "lemma Foo:\n" ...
For me "\t" does not work as an accept character (nothing happens when I
type "\t"... that's the only reason why I use "\n").
I would also prefer \t, but it does nothing for me.
See also
http://jedit.9.n6.nabble.com/jEdit-users-tab-do-not-complete-in-Sidekick-completion-popup-td2255082.html
from 23-Dec-2011, which is a bit odd to appear on jEdit-users, since
Matthieu Casanova is one of the jEdit cracks so I would have expected a
tracker item or jEdit-devel posting by him.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
