Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] 2013-1-RC1: clicking on a README file in the d...

Email Gateway (Aug 19 2022 at 12:16):

From: Christoph LANGE <math.semantic.web@gmail.com>
Hi Makarius,

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.

Cheers,

Christoph

Email Gateway (Aug 19 2022 at 12:17):

From: Makarius <makarius@sketis.net>
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

Last updated: Apr 24 2024 at 08:20 UTC