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