Email Gateway (Aug 22 2022 at 10:51): Email Gateway (Aug 22 2022 at 10:51):From: Gergely Buday <gbuday@gmail.com>
If you start typing
@{cite "DBLP
Isabelle/jEdit does not show any possible autocompletion.
However, if you type it with closing quoting sign and curly brace:
@{cite "DBLP"}
then the system will show all the possibilites.
I did not find this in the Isabelle/jEdit manual. If it indeed does not
contain it, it might be worth adding it as it was not obvious.
Now the sysem shows the entries in the order of the .bib file -- would it
be better to show them in alphabetic order?
Email Gateway (Aug 22 2022 at 11:21):From: Makarius <makarius@sketis.net>
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).
Makarius
Last updated: Apr 27 2024 at 01:05 UTC