Re: [isabelle] Remaining reasons for Proof General
I just gave the jEdit in 2013-1 a try. Here are my first impressions:
* In PG, I have some open buffers, these are the buffers that I'm
interested in. jEdit opens all dependent theories (approx 50 to 100 in
my typical use-case). So using cycle-buffer or similar functions makes
How can I efficiently switch between the theories that I'm currently
editing/interested in, without having to search them among dozens of
* I have no control when theories are processed. I loaded a theory,
and saw in the theory-panel all these purple bars slowly disappearing,
until no purple was left. Also for the theory that was currently
displayed in the main window. However, the theory in the main window was
NOT completely processed. When moving down the cursor, the purple bar
So how can I be sure that my theories are all correct?
On Di, 2013-11-12 at 16:01 +0100, Jasmin Blanchette wrote:
> 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