*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Peter Lammich <lammich at in.tum.de>*Date*: Tue, 12 Nov 2013 17:27:57 +0100*In-reply-to*: <97E4C903-231E-4CF2-9B86-E92AD8123D53@gmail.com>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com> <alpine.LNX.2.00.1311111227510.20958@macbroy21.informatik.tu-muenchen.de> <5280E51C.3010703@inf.ethz.ch> <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de> <97E4C903-231E-4CF2-9B86-E92AD8123D53@gmail.com>

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 no sense. How can I efficiently switch between the theories that I'm currently editing/interested in, without having to search them among dozens of uninteresting theories? * 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 appeared again. So how can I be sure that my theories are all correct? -- Peter 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. > > Jasmin >

**Follow-Ups**:**Re: [isabelle] Remaining reasons for Proof General***From:*Makarius

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Makarius

**Re: [isabelle] sledgehammer in RC4***From:*Andreas Lochbihler

**[isabelle] Remaining reasons for Proof General***From:*Makarius

**Re: [isabelle] Remaining reasons for Proof General***From:*Jasmin Blanchette

- Previous by Date: [isabelle] Wellsortedness error in code equation Gcd_nat_inst.Lcm_nat
- Next by Date: Re: [isabelle] find sessions
- Previous by Thread: Re: [isabelle] Remaining reasons for Proof General
- Next by Thread: Re: [isabelle] Remaining reasons for Proof General
- Cl-isabelle-users November 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list