[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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?

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.


 	Makarius