[isabelle-dev] Isabelle-10-Sept

[Makarius]

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 
ago.

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.


 	Makarius