Re: [isabelle] citation autocompletion

On Sat, 11 Jul 2015, Gergely Buday wrote:

If you start typing

 @{cite "DBLP

Isabelle/jEdit does not show any possible autocompletion.

That is utterly broken in input -- the system says that by an explicit error message in various spots, as the text is typed. Completion is not about repairing arbitrary input, but to make semantically sense of
something that has already some basic syntactic structure.

With the default configuration of Isabelle2015, I find it actually hard to type the partial input above: inserting "@{" already produces the closing "}". Maybe the PIDE should go as far as other IDEs and close the quoted string as well after the first ".

Now the sysem shows the entries in the order of the .bib file -- would it be better to show them in alphabetic order?

Yes, I will change that for the next release: first alphabetic order, then history order (according to frequency of previous selections by the user).


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