[isabelle-dev] NEWS: State panel

Makarius makarius at sketis.net
Mon Nov 9 21:41:38 CET 2015


* 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



More information about the isabelle-dev mailing list