Re: [ jEdit-devel ] FontSizePlugin

[Slava P. <sl...@je...>]

We already include macros with the core to do this. I'm sure you had fun 
coding the plugin, though. :-)

Oliver Epper wrote:
> Hi all !
> 
> Now, that I've figured out how to write jEdit plugins, I did another one
> which allows you to switch the view's font size on the fly.
> Like in Firefox, or T-Bird when pressinge <STRG><ALT>+, or -
> To achive this behavior you have to assign the shortcuts to the menu
> entries FontSize/bigger Font, FontSize/smaller Font.
> 
> INFO: Due to the excellent jEdit API (plugin, as well as core) this
> is by far no rocket science... You could easily achive the same
> effect by evaluating the following beanshell:
> ---
> jEdit.setProperty("view.fontsize", 14);
> jEdit.propertiesChanged();
> ---
> which is what the plugin does, basically...
> 
> If anyone besides my best buddy (he has a dramatically smaller
> screen resolution than me, but uses my jEdit scheme) thinks this is
> usefull I can add an option pane letting you choose the bigness by
> which your actual font is changed...
> 
> http://oliver.epper.de/FontSizePlugin.zip
> 
> - Oliver Epper
> 
> 
> -------------------------------------------------------
> SF email is sponsored by - The IT Product Guide
> Read honest & candid reviews on hundreds of IT Products from real users.
> Discover which products truly live up to the hype. Start reading now.
> http://ads.osdn.com/?ad_id=6595&alloc_id=14396&op=click