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
"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". 


> 
> 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.


Peter







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