[isabelle-dev] NEWS: State panel

[Gerwin Klein]

> On 9 Nov 2015, at 9:41 pm, Makarius <makarius at sketis.net> wrote:
>
> * The State panel manages explicit proof state output, with jEdit action
> "isabelle.update-state" (shortcut S+ENTER) to trigger update according
> to cursor position.
>
> * The Output panel no longer shows proof state output by default. This
> reduces resource requirements of prover time and GUI space.
> INCOMPATIBILITY, use the State panel instead or enable option
> "editor_output_state".
>
>
> This refers to Isabelle/bb20f11dd842.  The State panel has been around for a while, without mentioning it explicitly.  It should now be sufficiently consolidated for production use; even old GUI timing problems that caused excessive flashing due to repaints should no longer happen.

The separation looks like a good idea, but triggering state panel updates only on request doesn’t seem to mesh with how I use the interface these days. I’ve become very accustomed to the ability to immediately see the proof state by just navigating to the relevant command. It’s one of the things I really like about Isabelle/jEdit.

Maybe it’s because the shortcut doesn’t seem to be working for me (do I need to clear anything in my jedit settings first to get new defaults?), but even with a shortcut, I’ll now need two interactions to look at different proof states, when before I only needed one (navigate + shortcut as opposed to just navigate).

It’s true that producing proof state output for every single command in the document is a lot of overhead. Would triggering an update for each cursor movement (navigation/typing) be as bad as before in terms of overhead (or worse), or would it still be less?

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.