Re: [isabelle] jEdit: Abbreviations
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
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
> 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.
Unfortunately, I found no option that could enable completions within
words, or change what Sidekick/Completion considers to be a word.
> Completion content is provided by Isabelle/jEdit, though. It just uses
> certain global tables, without contextual information.
But SideKick obviously interprets the content of these tables wrt. some
context. For example, it does not propose a completion within a word:
If you type "dd", it proposes \<ddagger>, but if you type cudd, no
popup occurs. For me, it gets a problem, as the leading tick of a type
variable also inhibits the completion popup to occur.
This archive was generated by a fusion of
Pipermail (Mailman edition) and