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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
