diff --git a/index.html b/index.html
index 0f43126..35daea8 100644
--- a/index.html
+++ b/index.html
@@ -128,6 +128,11 @@
+
+
+
+
+
diff --git a/src/AppSettings.ts b/src/AppSettings.ts
index 951c59e..e3626a5 100644
--- a/src/AppSettings.ts
+++ b/src/AppSettings.ts
@@ -22,6 +22,7 @@ export interface Settings {
font_size: number
universes: Universes
selected_universe: string
+ line_numbers: boolean
}
export const template_universe = {
@@ -70,6 +71,7 @@ export class AppSettings {
public font_size: number = 22
public universes: Universes
public selected_universe: string = "Default"
+ public line_numbers: boolean = true
constructor() {
@@ -83,6 +85,7 @@ export class AppSettings {
this.font_size = settingsFromStorage.font_size
this.universes = settingsFromStorage.universes
this.selected_universe = settingsFromStorage.selected_universe
+ this.line_numbers = settingsFromStorage.line_numbers
} else {
this.universes = template_universes
}
@@ -97,7 +100,8 @@ export class AppSettings {
font: this.font,
font_size: this.font_size,
universes: this.universes,
- selected_universe: this.selected_universe
+ selected_universe: this.selected_universe,
+ line_numbers: this.line_numbers
}
}
@@ -107,6 +111,7 @@ export class AppSettings {
this.font = settings.font;
this.font_size = settings.font_size;
this.selected_universe = settings.selected_universe;
+ this.line_numbers = settings.line_numbers;
localStorage.setItem('topos', JSON.stringify(this.data))
}
}
\ No newline at end of file
diff --git a/src/EditorSetup.ts b/src/EditorSetup.ts
index 7b824d6..fb7ce23 100644
--- a/src/EditorSetup.ts
+++ b/src/EditorSetup.ts
@@ -1,4 +1,3 @@
-import { javascript } from "@codemirror/lang-javascript";
import {
keymap,
highlightSpecialChars,
@@ -6,7 +5,6 @@ import {
highlightActiveLine,
dropCursor,
rectangularSelection,
- lineNumbers,
crosshairCursor,
highlightActiveLineGutter,
} from "@codemirror/view";
@@ -16,13 +14,11 @@ import {
syntaxHighlighting,
indentOnInput,
bracketMatching,
- foldKeymap,
} from "@codemirror/language";
import { defaultKeymap, historyKeymap, history } from "@codemirror/commands";
-import { searchKeymap, highlightSelectionMatches } from "@codemirror/search";
+import { highlightSelectionMatches } from "@codemirror/search";
import {
autocompletion,
- completionKeymap,
closeBrackets,
closeBracketsKeymap,
} from "@codemirror/autocomplete";
@@ -68,11 +64,9 @@ import { lintKeymap } from "@codemirror/lint";
/// as desired.
export const editorSetup: Extension = (() => [
- lineNumbers(),
highlightActiveLineGutter(),
highlightSpecialChars(),
history(),
- // foldGutter(),
drawSelection(),
dropCursor(),
EditorState.allowMultipleSelections.of(true),
@@ -89,8 +83,6 @@ export const editorSetup: Extension = (() => [
...closeBracketsKeymap,
...defaultKeymap,
...historyKeymap,
- ...foldKeymap,
- ...completionKeymap,
...lintKeymap,
]),
])();
diff --git a/src/main.ts b/src/main.ts
index 6310e13..dd5b7ab 100644
--- a/src/main.ts
+++ b/src/main.ts
@@ -5,7 +5,7 @@ import { EditorState, Compartment } from "@codemirror/state";
import { javascript } from "@codemirror/lang-javascript";
import { markdown } from "@codemirror/lang-markdown";
import { Extension } from "@codemirror/state";
-import { ViewUpdate } from "@codemirror/view";
+import { ViewUpdate, lineNumbers } from "@codemirror/view";
import { oneDark } from "@codemirror/theme-one-dark";
import { vim } from "@replit/codemirror-vim";
import { Clock } from "./Clock";
@@ -27,6 +27,7 @@ export class Editor {
local_index: number = 1;
editor_mode: "global" | "local" | "init" | "notes" = "local";
fontSize: Compartment;
+ withLineNumbers: Compartment;
vimModeCompartment : Compartment;
chosenLanguage: Compartment
@@ -104,6 +105,9 @@ export class Editor {
font_size_slider: HTMLInputElement = document.getElementById('font-size-slider') as HTMLInputElement;
font_size_witness: HTMLSpanElement = document.getElementById('font-size-witness') as HTMLSpanElement;
+ // Line Numbers checkbox
+ line_numbers_checkbox: HTMLInputElement = document.getElementById('show-line-numbers') as HTMLInputElement;
+
// Editor mode selection
normal_mode_button: HTMLButtonElement = document.getElementById('normal-mode') as HTMLButtonElement;
vim_mode_button: HTMLButtonElement = document.getElementById('vim-mode') as HTMLButtonElement;
@@ -134,10 +138,12 @@ export class Editor {
// CodeMirror Management
// ================================================================================
- this.fontSize = new Compartment();
this.vimModeCompartment = new Compartment();
+ this.withLineNumbers = new Compartment();
this.chosenLanguage = new Compartment();
+ this.fontSize = new Compartment();
const vimPlugin = this.settings.vimMode ? vim() : [];
+ const lines = this.settings.line_numbers? lineNumbers() : [];
const fontSizeModif = EditorView.theme( {
"&": {
fontSize: `${this.settings.font_size}px`,
@@ -148,6 +154,7 @@ export class Editor {
})
this.editorExtensions = [
+ this.withLineNumbers.of(lines),
this.fontSize.of(fontSizeModif),
this.vimModeCompartment.of(vimPlugin),
editorSetup,
@@ -358,6 +365,7 @@ export class Editor {
this.font_size_slider.value = this.settings.font_size.toString();
this.font_size_witness.innerHTML = `Font Size: ${this.settings.font_size}px`
this.font_size_witness?.setAttribute('style', `font-size: ${this.settings.font_size}px;`)
+ this.line_numbers_checkbox.checked = this.settings.line_numbers;
let modal_settings = document.getElementById('modal-settings');
let editor = document.getElementById('editor');
modal_settings?.classList.remove('invisible')
@@ -392,6 +400,16 @@ export class Editor {
this.view.dispatch({effects: this.vimModeCompartment.reconfigure([])});
})
+ this.line_numbers_checkbox.addEventListener("change", () => {
+ let checked = this.line_numbers_checkbox.checked ? true : false;
+ this.settings.line_numbers = checked;
+ this.view.dispatch({
+ effects: this.withLineNumbers.reconfigure(
+ checked ? [lineNumbers()] : []
+ )
+ });
+ });
+
this.vim_mode_button.addEventListener("click", () => {
this.settings.vimMode = true;
this.view.dispatch({effects: this.vimModeCompartment.reconfigure(vim())});