Slightly better font selection but still buggy

Bubobubobubobubo · Oct 21, 2023 · 67d6836 · 67d6836
1 parent 8674e64
commit 67d6836
Show file tree

Hide file tree

Showing 4 changed files with 64 additions and 12 deletions.
diff --git a/index.html b/index.html
@@ -223,10 +223,8 @@ <h2 class="font-semibold lg:text-xl text-gray-400">More</h2>
                 <label for="font" class="block ml-5 mb-2 font-medium sd:text-sm">Font:</label>
                   <select id="font-family" class="bg-gray-50 ml-4 border border-gray-300 mb-2
                   text-gray-900 text-sm rounded-lg focus:ring-blue-500 focus:border-blue-500 block  p-2.5 dark:bg-gray-700 dark:border-gray-600 dark:placeholder-gray-400 dark:text-white">
-                    <option selected>Choose a font</option>
-                    <option value="US">IBM Plex Mono</option>
-                    <option value="CA">Victor Mono</option>
-                    <option value="FR">Courier</option>
+                    <option value="IBM Plex Mono">IBM Plex Mono</option>
+                    <option value="Courier">Courier</option>
                   </select>
               </div>
               <!-- Editor mode selection -->

diff --git a/src/EditorSetup.ts b/src/EditorSetup.ts
@@ -73,7 +73,7 @@ export const installEditor = (app: Editor) => {
       fontSize: `${app.settings.font_size}px`,
     },
     $content: {
-      fontFamily: `${app.settings.font}, Menlo, Monaco, Lucida Console, monospace`,
+      fontFamily: `${app.settings.font}`,
       fontSize: `${app.settings.font_size}px`,
     },
     ".cm-gutters": {
@@ -117,4 +117,22 @@ export const installEditor = (app: Editor) => {
     parent: document.getElementById("editor") as HTMLElement,
     state: app.state,
   });
+
+  // Re-apply font size and font family change
+  app.view.dispatch({
+    effects: app.fontSize.reconfigure(
+      EditorView.theme({
+        "&": {
+          fontSize: `${app.settings.font_size}px`,
+        },
+        $content: {
+          fontFamily: `${app.settings.font}`,
+          fontSize: `${app.settings.font_size}px`,
+        },
+        ".cm-gutters": {
+          fontSize: `${app.settings.font_size}px`,
+        },
+      })
+    ),
+  });
 };
diff --git a/src/FileManagement.ts b/src/FileManagement.ts
@@ -133,8 +133,8 @@ export class AppSettings {
    */
 
   public vimMode: boolean = false;
-  public theme: string = "materialDark";
-  public font: string = "Victor Mono";
+  public theme: string = "toposTheme";
+  public font: string = "IBM Plex Mono";
   public font_size: number = 24;
   public universes: Universes;
   public selected_universe: string = "Default";

diff --git a/src/InterfaceLogic.ts b/src/InterfaceLogic.ts
@@ -212,16 +212,52 @@ export const installInterfaceLogic = (app: Editor) => {
     //@ts-ignore
     let new_font = (app.interface.font_family_selector as HTMLSelectElement)
       .value;
+    console.log("Picking new font : " + new_font);
+    app.settings.font = new_font;
+
+    app.view.dispatch({
+      effects: app.fontSize.reconfigure(
+        EditorView.theme({
+          "&": { fontSize: app.settings.font_size + "px" },
+          ".cm-content": {
+            fontFamily: new_font,
+            fontSize: app.settings.font_size + "px",
+          },
+          ".cm-gutters": { fontSize: app.settings.font_size + "px" },
+        })
+      ),
+    });
   });
 
   app.interface.font_size_input.addEventListener("input", () => {
     let new_value: string | number = (
       app.interface.font_size_input as HTMLInputElement
     ).value;
     app.settings.font_size = parseInt(new_value);
+    // TODO: update the font size
+    app.view.dispatch({
+      effects: app.fontSize.reconfigure(
+        EditorView.theme({
+          "&": { fontSize: app.settings.font_size + "px" },
+          ".cm-content": {
+            fontFamily: app.settings.font,
+            fontSize: app.settings.font_size + "px",
+          },
+          ".cm-gutters": { fontSize: app.settings.font_size + "px" },
+        })
+      ),
+    });
   });
 
   app.interface.settings_button.addEventListener("click", () => {
+    // Populate the font selector
+    const fontFamilySelect = document.getElementById(
+      "font-family"
+    ) as HTMLSelectElement | null;
+    if (fontFamilySelect) {
+      fontFamilySelect.value = app.settings.font;
+    }
+
     // Populate the font family selector
     const doughNudgeRange = app.interface.dough_nudge_range as HTMLInputElement;
     doughNudgeRange.value = app.dough_nudge.toString();
@@ -230,9 +266,6 @@ export const installInterfaceLogic = (app: Editor) => {
       "doughnumber"
     ) as HTMLInputElement;
     doughNumber.value = app.dough_nudge.toString();
-    (app.interface.font_family_selector as HTMLSelectElement).value =
-      app.settings.font;
-
     if (app.settings.font_size === null) {
       app.settings.font_size = 12;
     }
@@ -273,12 +306,15 @@ export const installInterfaceLogic = (app: Editor) => {
     let editor = document.getElementById("editor");
     modal_settings?.classList.add("invisible");
     editor?.classList.remove("invisible");
-    // Update the font size once again
+    let new_value: string = (app.interface.font_size_input as HTMLInputElement)
+      .value;
+    app.settings.font_size = parseInt(new_value);
+    // Update fontSize compartment with new font size value
     app.view.dispatch({
       effects: app.fontSize.reconfigure(
         EditorView.theme({
           "&": { fontSize: app.settings.font_size + "px" },
-          "&content": {
+          ".cm-content": {
             fontFamily: app.settings.font,
             fontSize: app.settings.font_size + "px",
           },