Re: [isabelle] jEdit: Abbreviations
On Thu, 14 Feb 2013, Peter Lammich wrote:
I type: "'gamma", there comes no popup proposing \<gamma>. The only
workaround I currently know is something like typing "' gamma", and then
using backspace to erase the extra space again.
You can just ignore the propsition, it should be mostly non-intrusive.
See also what Isabelle2013/NEWS has to say:
* More reactive completion popup by default: use \t (TAB) instead of
\n (NEWLINE) to minimize intrusion into regular flow of editing. See
also "Plugin Options / SideKick / General / Code Completion Options".
For Isabelle2013, I merely made sure that \t actually works. Everything
else is then delegated to the Sidekick/Completion plugin of jEdit. It has
many options to customize its dynamic behaviour.
Completion content is provided by Isabelle/jEdit, though. It just uses
certain global tables, without contextual information.
This archive was generated by a fusion of
Pipermail (Mailman edition) and