[isabelle-dev] Remaining uses of Proof General?

[Gerwin Klein]

On 25 Jul 2014, at 11:20 am, Makarius <makarius at sketis.net> wrote:

> On Fri, 25 Jul 2014, Gerwin Klein wrote:
>
>>
>> On 25 Jul 2014, at 10:23 am, Makarius <makarius at sketis.net> wrote:
>>
>>> Oddly, people are still seen using 'find_theorems' etc. inlined into the source text.  That was an intermediate approach from several years ago. If it is still used today, what are the remaining resons for it?
>>
>> Not having to touch the mouse is the main reason for me why I still use thm, find_theorems, sledgehammer etc commands.
>
> Does that actually refer to Isabelle2014-RC0, or some older version?

My motivation (keyboard-only use) is the same for both.


> I have reworked the focus handling such that the panels that require some input move the focus in the right spot.  It should be also possible to define some keyboard shotcurts to activate the panel in question.

Yes, but typing find_theorems is fast, esp with completion and needs no further setup or visual context switching. I don’t actually have any problem with either option, I’m just finding myself using the explicit diagnostic commands still fairly often instead of the panels because of that. For demos, I use the panels much more often.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.