Email Gateway (Aug 18 2022 at 18:47): Email Gateway (Aug 18 2022 at 18:47):From: Christian STERNAGEL <c-sterna@jaist.ac.jp>
Hi all,
I seem to be unable to find out how to enable nice symbols in jedit (in
Isabelle2011-1). Where the popups with selection possibilities disabled
by default, or is their absence a problem of my installation (maybe
java)? I was used to type e.g. "=" followed by ">" and then get a box
where I could choose the nice Rightarrow. This no longer happens. Any ideas?
cheers
chris
Email Gateway (Aug 18 2022 at 18:47):From: James Frank <james.isa@gmx.com>
I attached a screenshot for how I have my Sidekick options set.
In the "Code Completion Options" box, you have to enable "Show
completion popups where possible" .
In the field "Accept characters for completion popup", you might want to
change it back to "\ \n\t".
--James
sidekickOptions.png
Email Gateway (Aug 18 2022 at 18:47):From: Christian STERNAGEL <c-sterna@jaist.ac.jp>
Thanks! That worked. Note that in my case setting "accept characters for
completion popup" to "\n\t" (instead of "\ \n\t") did only work after
setting "accept character to insert after completion" to the empty
string. But this combination is really useful (thanks James), since now
by hitting "enter" I can choose to use the completion and by hitting
"space" to ignore it (which was not so convenient, in terms of hand
movements, before).
cheers
chris
Last updated: Apr 19 2024 at 20:15 UTC