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.


	Makarius






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.