Re: [isabelle] Remaining reasons for Proof General

On Tue, 12 Nov 2013, Jasmin Blanchette wrote:

The main reason for this is that it's much easier to reload ML code in PG than in jEdit.

Isabelle/PG was good at reloading exactly those theories that need to be reloaded, without baby sitting. Trying to achieve the same in jEdit requires a lot of clicking and a bit of thinking (to figure which .thy file has the right "ML_file" command).

I understand my use case is not typical for most users, who do not spend their days writing long pieces of ML code, and I can live with PG to do that. Still, it would be nice if jEdit/PIDE, which is otherwise so smart about so many Isabelle specifics, would reach the level of PG on this one point.

The non-handling of add-on files, especially ML ones, is one of the main omissions from the past 5 years of Isabelle/jEdit. Just a few weeks ago, while cycling through sunny Apulia, I've devised a reasonably simple way to get there. Lets see if I manage for the next release.

The reason why its not there yet is indeed the coincidence that it mostly affects people working on Isabelle/HOL itself, which are releatively few, and it is a relatively tough job anyway. It does not mean that I am not annoyed myself by the omission.

Some months ago, I had a different and quite pleasant experience with Isabelle/ML development in Isabelle/jEdit. Doing just plain 'ML' sections (to avoid the ML file problem) and some 'keywords' in the header, it was really nice to work out some Isar commands. The only surprise was a sudden breakdown due to an old version of the command still persisting while the new version was malformed (rejected by the ML compiler).

The internal command table is still global for historic reasons (Proof General legacy again) and poking into it can have unexpected effects.


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