Re: [isabelle] RC2 for testing; Toplevel.timing has no affect anymore



On Fri, 11 Oct 2013, Makarius wrote:

If I hit F11 to maximize the screen, the circular icon will start moving slowly, but there aren't any ATPs running, so I click "Apply", and then the circular icon starts moving faster.

I have seen that myself in Isabelle2013-1-RC2, and will investigate it further.

The current success rate for full-screen mode is a bit more than 50%. On some platforms it does not work at all, and when it works it can cause some surprises (like windows that are unreachable somewhere behind the main window).

I now understand better what F11 (toggle full-screen mode) does here.

The deeper problem is that the state of the Sledgehammer panel is managed in accordance to its GUI representation, but that is reset a bit more often than anticipated. When you toggle full-screen mode, the panel is removed and added again, so the Sledgehammer run is reset. In Isabelle2013-1-RC2 the GUI display is a bit crude and merely changes into the state "Waiting for evaluation of context ...". In the coming RC3 this week it will be more clear that the state is reset.

These slight inconveniences of dockable window state are due to certain features of Java/Swing and jEdit Dockable Window Management. For Output and Info, I had already made some workarounds a few years ago, to pretend more persistence than is there in reality. Instead of adding more workarounds it would be better to brush up the Dockable Window Manager at some point, but it requires some enthisiastic and competent people helping out at the jEdit project on Sourceforge.

Another known problem of dockable windows (especially in full-screen mode) is that windows often get lost behind the main window. The precise behaviour is platform dependent.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.