[jEdit-Syntax-devel] Changing Font

[Ruffin B. <ru...@co...>]

I was playing around in the code today, and found that it's pretty easy 
to change font by changing the follow line in the TextAreaPainter.java 
file:

setFont(new Font("Monospaced",Font.PLAIN,14));

However there doesn't seem to be any way of changing the font on the 
fly -- or even on startup at the moment.  It seems the monospaced, 14 pt 
font is hardcoded in there for now (?) after my initial check of the 
source.

I'm planning on adding a new constructor to TextAreaPainter that accepts 
a font specification, and have the creation of a JEditText pass the 
values around this line:

painter = new TextAreaPainter(this,defaults);

I thought it'd make the most sense to drop this stuff in the 
TextAreaDefaults class.

Does that make sense?  Is there a better way to change fonts, especially 
on the fly [without dropping the old JEditTextArea in my frame and 
adding a new one] that I'm missing?

Thanks,

Ruffin Bailey