@@ -157,8 +157,6 @@ static public void guardedMain(String args[]) throws Exception {
157157
158158 BaseNoGui .initParameters (args );
159159
160- System .setProperty ("swing.aatext" , PreferencesData .get ("editor.antialias" , "true" ));
161-
162160 BaseNoGui .initVersion ();
163161
164162// if (System.getProperty("mrj.version") != null) {
@@ -207,6 +205,7 @@ static public void guardedMain(String args[]) throws Exception {
207205
208206 // setup the theme coloring fun
209207 Theme .init ();
208+ System .setProperty ("swing.aatext" , PreferencesData .get ("editor.antialias" , "true" ));
210209
211210 // Set the look and feel before opening the window
212211 try {
@@ -1751,9 +1750,11 @@ public void paint(Graphics g) {
17511750 g2 .setRenderingHint (RenderingHints .KEY_TEXT_ANTIALIASING ,
17521751 RenderingHints .VALUE_TEXT_ANTIALIAS_OFF );
17531752
1754- g .setFont (new Font ("SansSerif" , Font .PLAIN , 11 ));
1753+ int scale = Theme .getInteger ("gui.scalePercent" );
1754+ Font f = new Font ("SansSerif" , Font .PLAIN , 11 * scale / 100 );
1755+ g .setFont (f );
17551756 g .setColor (Color .white );
1756- g .drawString (BaseNoGui .VERSION_NAME_LONG , 33 , 20 );
1757+ g .drawString (BaseNoGui .VERSION_NAME_LONG , 33 * scale / 100 , 20 * scale / 100 );
17571758 }
17581759 };
17591760 window .addMouseListener (new MouseAdapter () {
@@ -2049,6 +2050,9 @@ static public Image getThemeImage(String name, Component who) {
20492050 static public Image getLibImage (String name , Component who ) {
20502051 Toolkit tk = Toolkit .getDefaultToolkit ();
20512052
2053+ int scale = Theme .getInteger ("gui.scalePercent" );
2054+ // TODO: create high-res enlarged copies and load those if
2055+ // the scale is more than 125%
20522056 File imageLocation = new File (getContentFile ("lib" ), name );
20532057 Image image = tk .getImage (imageLocation .getAbsolutePath ());
20542058 MediaTracker tracker = new MediaTracker (who );
@@ -2057,6 +2061,15 @@ static public Image getLibImage(String name, Component who) {
20572061 tracker .waitForAll ();
20582062 } catch (InterruptedException e ) {
20592063 }
2064+ if (scale != 100 ) {
2065+ int width = image .getWidth (null ) * scale / 100 ;
2066+ int height = image .getHeight (null ) * scale / 100 ;
2067+ image = image .getScaledInstance (width , height , Image .SCALE_SMOOTH );
2068+ tracker .addImage (image , 1 );
2069+ try {
2070+ tracker .waitForAll ();
2071+ } catch (InterruptedException e ) { }
2072+ }
20602073 return image ;
20612074 }
20622075
0 commit comments