[DrJava] [ drjava-Feature Requests-681488 ] Configurable line number font

[SourceForge.net <no...@so...>]

Feature Requests item #681488, was opened at 2003-02-06 06:03
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=438938&aid=681488&group_id=44253

Category: Definitions (source editor)
Group: Small (< 1 pair-week)
Status: Open
Priority: 5
Submitted By: Charles Reis (csreis)
Assigned to: Nobody/Anonymous (nobody)
Summary: Configurable line number font

Initial Comment:
Story:
User turns on "Line Number Enumeration" in the Display
Options section of the Preferences Window, and line
numbers are displayed in the left margin.  However, the
user finds the font to be difficult to read, so he
changes "Line Number Font" in the Fonts section of the
Preferences Window to specify a larger font size.

Implementation notes:
Be careful of the hard-coded widths in the LineEnumRule
class...

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=438938&aid=681488&group_id=44253