[isabelle-dev] NEWS: State panel

[Makarius]

On Tue, 10 Nov 2015, Fabian Immler wrote:

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

In Isabelle/1d81de0bddc4 both the keyboard action and the button do the 
same thing: an update with explicit request to print the state again.


There could be still situations, where the display is not in sync with the 
document mode, due to somewhat different approach than the Output panel. 
The State panel is more like Query.

When new questions arise, we should discuss carefully what is right and 
what is wrong.


 	Makarius