Email Gateway (Aug 22 2022 at 15:21): Email Gateway (Aug 22 2022 at 15:21):From: Rafal Kolanski <xs@xaph.net>
Dear Isabelle Users,
While I may fly in the face of canon here, I remember being previously
happy with using <CR> as my "accept completion" binding in 2016.
However, in 2016-1 typing a double quote character semi-immediately
drops down a completion menu related to cartouches. I already use `
(backtick) for cartouches. Double quotes regularly in use in our
developments (definitions/primrecs/fun/etc.). I can escape the
completion with ESC, but I am often faster than the dropdown and it's
getting frustrating.
Is it possible to turn off cartouche autocompletion for double quotes?
I'm willing to modify anything and perform surgery on the Isabelle jEdit
plugin if someone can point me to where this originates from, because
I'm struggling to find it.
Many thanks for any advice,
Rafal Kolanski
Email Gateway (Aug 22 2022 at 15:21):From: Makarius <makarius@sketis.net>
See these hard-wired default_abbrevs:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/General/completion.scala#l315
You need to rebuild Isabelle/jEdit from the repository after changing
the Scala source.
Makarius
Last updated: Apr 18 2024 at 16:19 UTC