Re: [isabelle] jEdit: Abbreviations



On Thu, 14 Feb 2013, Peter Lammich wrote:

On Do, 2013-02-14 at 13:01 +0100, Makarius wrote:
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.

Sorry if I phrased my question not clearly enough. I *want* jEdit to
propose the completion γ (\<gamma>) when I type "gamma".
However, it does not do so if I type "'gamma", nor on "foo_gamma" nor
"digamma".

While it probably makes sense not to get a completion proposal for
"gamma" if you type "digamma", I definitely want to have a completion
proposal when I type "'gamma", and would like to have one for
"foo_gamma".

Now I understand what you are trying to do. Isabelle/jEdit treats "'" as part of a "word" according to the usual syntax for identifiers.

Since the application is just for a few exceptional cases, you can try to use the on-board Abbreviation mechanism, or any other plugin. It is a matter to explore possibilities of what is there already.


	Makarius


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