Change the font family and scale

NOTE: This does *not* change spacing between lines, so larger text sizes may look strange
Gaming32 · Dec 30, 2021 · ced2264 · ced2264
1 parent 1a32c6f
commit ced2264
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 3 deletions.
diff --git a/src/main/ArrayVisualizer.java b/src/main/ArrayVisualizer.java
@@ -194,6 +194,7 @@ final public class ArrayVisualizer {
 
     private Statistics statSnapshot;
     private String fontSelection;
+    private int fontSelectionScale;
 
     private volatile boolean TEXTDRAW;
     private volatile boolean COLOR;
@@ -378,11 +379,25 @@ public void run() {
         this.arrays = new ArrayList<>();
         this.arrays.add(this.array);
 
+        this.fontSelection = "Times New Roman";
+        this.fontSelectionScale = 25;
         List<Integer> statsInfoList = new ArrayList<>();
         try (Scanner statsScanner = new Scanner(new File("stats-config.txt"))) {
             while (statsScanner.hasNextLine()) {
                 String line = statsScanner.nextLine().trim();
                 if (line.length() > 0 && line.charAt(0) == '#') continue;
+                if (line.startsWith("FONT: ")) {
+                    String font = line.substring(5);
+                    int fontScale = 25;
+                    int starIndex;
+                    if ((starIndex = font.indexOf('*')) != -1) {
+                        fontScale = Integer.parseInt(font.substring(starIndex + 1).trim());
+                        font = font.substring(0, starIndex);
+                    }
+                    fontSelection = font.trim();
+                    fontSelectionScale = fontScale;
+                    continue;
+                }
                 Integer type = STAT_CONFIG_KEYS.get(line.toLowerCase());
                 if (type == null) {
                     System.err.println("Unknown statistic type: " + type);
@@ -474,8 +489,7 @@ public void run() {
         this.category = "";
         this.heading = "";
         this.extraHeading = "";
-        this.fontSelection = "Times New Roman";
-        this.typeFace = new Font(this.fontSelection, Font.PLAIN, (int) (this.getWindowRatio() * 25));
+        this.typeFace = new Font(fontSelection, Font.PLAIN, (int) (this.getWindowRatio() * fontSelectionScale));
 
         this.statSnapshot = new Statistics(this);
 
@@ -1110,7 +1124,7 @@ public double getWindowRatio() {
         return this.cw / 1280d;
     }
     public void updateFontSize() {
-        this.typeFace = new Font(this.fontSelection, Font.PLAIN, (int) (this.getWindowRatio() * 25));
+        this.typeFace = new Font(fontSelection, Font.PLAIN, (int) (this.getWindowRatio() * fontSelectionScale));
         this.mainRender.setFont(this.typeFace);
     }
 

diff --git a/stats-config.txt b/stats-config.txt
@@ -1,3 +1,4 @@
+FONT: Times New Roman * 25
 # fps
 #
 sort
-Original file line number
+Diff line change
@@ -1,3 +1,4 @@
+    FONT: Times New Roman * 25
     # fps
     #
     sort
@@ Expand Down @@