[isabelle-dev] NEWS: State panel

[Fabian Immler]

Hi Makarius,

I noticed some strange behavior: if one triggers state output on the same command but after changing the state, the state output does not change. Consider this example:

lemma
  assumes False
  shows "False ∧ False"
  (*using assms*)
  apply simp

If you trigger output on the "apply simp" command, you get 1 subgoal in the State panel.
Now uncomment "using assms" and trigger output again (on the "apply simp" command): the State panel does not change.

I just noticed that this behavior only occurs when the output is triggered with a keyboard shortcut, clicking on the "Update" button yields the expected behavior.

Having worked with the "new" interaction model for half a day, I am wondering if it could make sense to trigger output in the State panel also implicitly with cursor movements?
That would require less explicit interaction with the IDE but still save (some?) resources (if I am guessing correctly that previously all intermediate proof states have been pretty printed and rendered in the background while now it would only happen on demand).

Best regards,
Fabian


> Am 09.11.2015 um 21:41 schrieb Makarius <makarius at sketis.net>:
> 
> * 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