Re: [isabelle] 2013-1-RC1: clicking on a README file in the documentation panel doesn't go to it if it's open already



On Fri, 4 Oct 2013, Christoph LANGE wrote:

a minor bug in Isabelle2013-1-RC1: suppose I open a README-like file in the documentation panel, and then switch to some other file. When I click the file's documentation panel entry once more, nothing happens, probably because the documentation panel thinks "the file is already open anyway". But I would expect that this action takes me back to the file.

Again the meaningless "b**" word. (The problem with the "bug" and "fix" pair is that it gives you the false impression of a clearly isolated problem that gets solved once and for all afterwards, but this is hardly ever the case in reality).


I've noticed this slightly surprising behaviour myself, but did not manage to improve the situation fundamentally for this release. The existance of the documumentation panel is already a step forward, and we never stop moving forward anyway, so further refinements can be left for future releases.

The Documentation panel is one of the many things that look trivial, but expose a long story of grand failure of modern operating systems: so far I did not find a reliable way to open PDF documents on all platforms without any potential for surprise. On Mac OS X, I even have to bypass the standard PDF viewer and "abuse" Safari for that job -- this will probably change again when we no longer support Snow Leopard.

In general, jEdit has minimal control on launching the viewer and no proper way to confirm its success. So it only takes the first click on the tree view into account, fires up the viewer, and hopes for the best. In most practical situations, this will approximate on idempoent open operation on the PDF.

I could have made a special case for internal text files of jEdit, but this is in danger to cause more trouble elsewhere, with an exponential blowup of special cases here and there. (I actually did consider it briefly for that very special special case, but dismissed the idea a few days ago.)


	Makarius





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