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