[isabelle-dev] NEWS: State panel

[Mathias Fleury]

Hello Makarius,

this might be intended, but in Isabelle/a99125aa964f from this morning the errors and warnings still goes to the output panel, which means that both panel have to be opened at the same time. 


Could you give us some insights about your workflow (for theorem proving) with the new state panel? I tried it this morning, but it did not fit nicely in my workflow, where I look at the output panel after typing a tactic to see if the goal is solved or what remains to prove. I would say that having ENTER bound to a command like "Insert Newline, Indent and update state panel" would be close enough to my workflow, but still solve the performance issues, you mentioned. Feedback from other users would be interesting here.


As a side question, is there a way to have two different panels docked at bottom open at the same time (i.e. splitting the bottom area into two parts and have two different panels in each)?


Thanks,
Mathias

> On 9 Nov 2015, at 21:41, 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.
> 
> Disabling option editor_output_state allows to get back to the traditional Isabelle/jEdit behaviour, but tradtionalists might actually like the new State panel better, because it is closer to Proof General (in the newer 3-buffer model, not the truely traditional 2-buffer model).
> 
> 
> 	Makarius
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev