Email Gateway (Aug 19 2022 at 07:52): Email Gateway (Aug 19 2022 at 07:52):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
There is one thing about jedit that really annoys me: when I type in an
abbreviation of a Unicode token (well, not all of them are Unicode
tokens, but you know what I mean), such as -_ or !!, I always have to
wait for the auto completion window and then press return for it to be
converted to the corresponding Unicode token.
This, frankly, is rather annoying since I don't need auto completion
anyway. I already set the completion dialogue delay to 0 and that helps
a bit, but I still have to press return every time and that's annoying.
I want jedit to replace the abbreviations with the corresponding Unicode
tokens immediately when I type them, like Proof General does, since this
enables me to type much faster.
Is there a way to do this, and if not, is it possible to add an option
for this in future releases of jedit?
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 07:52):From: Lars Noschinski <noschinl@in.tum.de>
You can set completion popup delay to 0ms (and then preferable change
completion keys from "\n\t " to "\t"); this makes input much more
comfortable.
Email Gateway (Aug 19 2022 at 07:52):From: Joachim Breitner <breitner@kit.edu>
Hi Lars,
ah, great suggestion, this has been bothering me as well. But I cannot
find this setting anywhere; where would I find it?
Thanks,
Joachim
signature.asc
Email Gateway (Aug 19 2022 at 07:52):From: Christian Sternagel <c-sterna@jaist.ac.jp>
Maybe I did not get the original question right. I thought it was: how
to obtain unicode tokens faster / by default?
If so, maybe reform to: change completion keys from <whatever> to "\n\t
", since with the previously suggested setting unicode tokens are only
inserted when tab ("\t") is pressed (which would be even more inconvenient).
Btw: The settings can be changed in "Plugins -> Plugin Options ->
SideKick -> General".
cheers
chris
Email Gateway (Aug 19 2022 at 07:53):From: Makarius <makarius@sketis.net>
BTW, "uncode token" is terminology from Proof General 4.x, and in Proof
General 3.x it was called "x-symbol".
Isabelle has always called things like \<forall> "Isabelle symbol" (since
1998, even before Proof General). In the current Isabelle/Scala/jEdit
technology, a finite selection of the infinitely many Isabelle symbols are
mapped to Unicode for "poor man's mathematical rendering" -- including
sub/superscripts/bold. This makes the text buffer physically unicode, but
the prover sources behind that are independent of it, using plain Isabelle
symbols as before.
Such fine points are occasionally relevant even for users, to avoid
surprises that things are slightly different than first anticipated.
Makarius
Email Gateway (Aug 19 2022 at 07:55):From: Lars Noschinski <noschinl@in.tum.de>
Plugins / Plugin Options / SideKick / General.
Under Code Cmopletion Options, set "After popup trigger keystrowk, wait"
to 0.0; enable "Automatic completion popups get focus".
-- Lars
Email Gateway (Aug 19 2022 at 07:55):From: Lars Noschinski <noschinl@in.tum.de>
This is all a matter of preference, but I prefer to use \t only as a
completion character, as otherwise I need to take care to avoid
completion in certain situations (the colon in lemma names, ML code ,...).
Last updated: Nov 21 2024 at 12:39 UTC