makarius at sketis.net
Tue Sep 24 22:49:24 CEST 2013
On Tue, 10 Sep 2013, Alfio Martini wrote:
> On the other hand, the (propositional) operators of HOL-formulae are
> still not properly shown in the sidekick pane as the image attached
> shows. I am not sure if this is a "feature" or a known bug, but this is
> problem is also present in the current version.
I think this visual glitch has been there all the time -- I did not notice
it myself so far, since I am not using Windows every day (but still quite
often to test things). No other Windows user has pointed that out yet,
maybe because Windows users traditionally think that problems are normal.
On the other hand the really anoying problems today are on Mac OS X and
Linux -- this is particularly bad because it used to be better a few years
In the longer term I would like to replace SideKick by a more versatile
tree view (or even graph view) of the PIDE document model. The completion
has already been replaced like that for the coming release. Getting rid
of Isabelle Sidekick altogether will take longer.
Since I've passed by the SideKick plugin sources today, I've had a brief
look what they are doing. In principle it should be reasonably easy to
modify SideKickTree.Renderer (and the corresponding "Asset") to allow an
explicit font specification. This would require to engage with the
maintainers of the plugin at the jEdit Sourceforge project, and will
probably take 1 or 2 release cycles of jEdit.
I am presently involved with the jEdit Sourceforge project, but for much
more elementary things, like getting Java 7 on Mac OS X work smoothly.
Everybody is hoping to discontinue Java 6 soon, but it is not for free to
dismantle old stuff.
More information about the isabelle-dev