Re: [isabelle] Isabelle2014-RC0 available for testing
On Tue, 8 Jul 2014, Joachim Breitner wrote:
And another thing worth noting, although already present in the 2013
release: When jumping to a file that is loaded as part of the loaded
heap (e.g. Set), there is an error at the theory command: “Cannot update
finished theory "Set"”. That makes sense to me, but I don’t plan to
update the theory, I just want to navigate it. Currently, this prevents
me from using Ctrl-Click on definitions in that file to navigate
This is a very old omission in the PIDE document model: the relation to
persistent heap images is not really addressed. I think this is becoming
more anoying now, since so many other things work smoothly.
One reason why a substantial reforms in this department are difficult are
are the 4 different "modes" of Isabelle: Isar TTY, Proof General, batch
build, PIDE interaction.
The first two are obsolete, but still around to hinder progress. The
second two might need more reconsiderations, if there are chances to unify
them into just one.
This archive was generated by a fusion of
Pipermail (Mailman edition) and