On 25 Jul 2014, at 11:20 am, Makarius <makar...@sketis.net> wrote: > On Fri, 25 Jul 2014, Gerwin Klein wrote: > >> >> On 25 Jul 2014, at 10:23 am, Makarius <makar...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
