[isabelle-dev] NEWS: State panel

[Tobias Nipkow]

On 10/11/2015 14:20, Gerwin Klein wrote:
>
>> 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.

I couldn't agree more, and others I spoke to confirm this. Thus it is 
unfortunate that this mode of working now requires an explicit flag that novices 
won't know about, apparently motivated by resource considerations. It would be 
better if people who run into resource problems (novices typically don't) can 
set a flag to disable the state being shown.

Tobias

> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5132 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20151110/f03e1563/attachment.bin>