Email Gateway (Aug 12 2023 at 14:59): Email Gateway (Aug 12 2023 at 14:59):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
I am observing that when a citation is made in a theory file (in a directory set up
following the usual AFP organization, with a root.bib and a root.tex file in the "document"
subdirectory); e.g. by
\<^cite>‹"xxx"›
then if there is some issue with the BibTeX file (for example, there is no reference "xxx"),
then an error is flagged in the JEdit window. However, if one goes and corrects the BibTeX
file (e.g. by adding the missing entry), the error message does not get reset, even if one
does "Reload All". It is necessary to close JEdit and restart it in order to reset the error
message.
I think this behavior probably was introduced with the introduction of \<^cite>, so it
might have already been in Isabelle2022. However, I have not tried to edit BibTeX files
since Isabelle2022 was released, so I didn't observe this until now.
Email Gateway (Sep 12 2023 at 18:38):From: Makarius <makarius@sketis.net>
Yes, that is an accurate description of the situation in Isabelle2023. There
have been may improvements concerning document preparation, e.g. the new
"Document" panel, but a few fine points are still unfinished.
In particular, bib files are not treated properly within the PIDE document
model: this is what counts for Isabelle/jEdit.
The underlying jEdit text editor has its own mechanisms for checking and
updates of files, e.g. in SideKick, but that is of little relevance to
Isabelle/jEdit. In particular, loading or re-loading of buffers has no direct
impact on the PIDE document model. (The idea is that it should not matter if a
PIDE file happens to be open or not, saved or unsaved etc.)
So this is the pragmatic answer for Isabelle2023: after significant changes to
bib files, you need to restart the Prover IDE.
Makarius
Last updated: Apr 28 2024 at 20:16 UTC