@@ -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 {
@@ -1763,9 +1762,11 @@ public void paint(Graphics g) {
17631762 g2 .setRenderingHint (RenderingHints .KEY_TEXT_ANTIALIASING ,
17641763 RenderingHints .VALUE_TEXT_ANTIALIAS_OFF );
17651764
1766- g .setFont (new Font ("SansSerif" , Font .PLAIN , 11 ));
1765+ int scale = Theme .getInteger ("gui.scalePercent" );
1766+ Font f = new Font ("SansSerif" , Font .PLAIN , 11 * scale / 100 );
1767+ g .setFont (f );
17671768 g .setColor (Color .white );
1768- g .drawString (BaseNoGui .VERSION_NAME_LONG , 33 , 20 );
1769+ g .drawString (BaseNoGui .VERSION_NAME_LONG , 33 * scale / 100 , 20 * scale / 100 );
17691770 }
17701771 };
17711772 window .addMouseListener (new MouseAdapter () {
@@ -2061,6 +2062,9 @@ static public Image getThemeImage(String name, Component who) {
20612062 static public Image getLibImage (String name , Component who ) {
20622063 Toolkit tk = Toolkit .getDefaultToolkit ();
20632064
2065+ int scale = Theme .getInteger ("gui.scalePercent" );
2066+ // TODO: create high-res enlarged copies and load those if
2067+ // the scale is more than 125%
20642068 File imageLocation = new File (getContentFile ("lib" ), name );
20652069 Image image = tk .getImage (imageLocation .getAbsolutePath ());
20662070 MediaTracker tracker = new MediaTracker (who );
@@ -2069,6 +2073,15 @@ static public Image getLibImage(String name, Component who) {
20692073 tracker .waitForAll ();
20702074 } catch (InterruptedException e ) {
20712075 }
2076+ if (scale != 100 ) {
2077+ int width = image .getWidth (null ) * scale / 100 ;
2078+ int height = image .getHeight (null ) * scale / 100 ;
2079+ image = image .getScaledInstance (width , height , Image .SCALE_SMOOTH );
2080+ tracker .addImage (image , 1 );
2081+ try {
2082+ tracker .waitForAll ();
2083+ } catch (InterruptedException e ) { }
2084+ }
20722085 return image ;
20732086 }
20742087
0 commit comments