On 10/11/2015 14:20, Gerwin Klein wrote:
On 9 Nov 2015, at 9:41 pm, Makarius <makar...@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-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
