diff --git a/index.html b/index.html
index ec6b5d7..2d3c60c 100644
--- a/index.html
+++ b/index.html
@@ -223,10 +223,8 @@
diff --git a/src/EditorSetup.ts b/src/EditorSetup.ts
index 5eae43e..944454d 100644
--- 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
index 0b88229..75db8a6 100644
--- 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
index 9b726fe..867020b 100644
--- a/src/InterfaceLogic.ts
+++ b/src/InterfaceLogic.ts
@@ -212,6 +212,21 @@ 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", () => {
@@ -219,9 +234,30 @@ export const installInterfaceLogic = (app: Editor) => {
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",
},