Re: [isabelle] Remaining reasons for Proof General

Hi Makarius,

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