Re: [isabelle] Remaining reasons for Proof General
I still find myself using Proof General on a daily basis. The main reason for this is that it's much easier to reload ML code in PG than in jEdit. Here's a typical scenario. Suppose I want to debug a failure in "primcorec". Then I do the following:
1. Open a "Scratch" theory by starting PG with -l HOL-Cardinals (the base image of BNF).
2. Import "~~/src/HOL/BNF/BNF_GFP" and write a small example that reproduces the problem in "Scratch".
3. Add debugging commands, fix bugs, etc., in the ML files loaded (directly or indirectly) by "BNF_GFP" using some other editor.
4. Unprocess and reprocess "Scratch".
5. Repeat steps 3 and 4 dozens of times.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and