> 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. 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
