show or hide line numbers

index.html

@@ -128,6 +128,11 @@
                   <label id="vim-mode" for="bordered-radio-2" class="w-full py-4 ml-2 text-sm font-medium text-black">Vim Mode</label>
                 </div>
               </div>
+              <!-- Line Numbers  -->
+              <div class="flex items-center mb-4 ml-8">
+                  <input id="show-line-numbers" type="checkbox" value="" class="w-4 h-4 text-blue-600 bg-gray-100 border-gray-300 rounded focus:ring-blue-500 dark:focus:ring-blue-600 dark:ring-offset-gray-800 focus:ring-2 dark:bg-gray-700 dark:border-gray-600">
+                  <label for="default-checkbox" class="ml-2 text-sm font-medium text-dark">Show Line Numbers</label>
+              </div>
               <!-- Information card -->
               <div class="flex lg:flex-row space-y-2 lg:space-y-0 flex-col w-auto min-w-screen px-4 lg:space-x-8 space-x-0">
                 <a href="https://github.com/Bubobubobubobubo/Topos" class="block max-w-sm p-6 border border-gray-200 rounded-lg shadow bg-gray-800 border-gray-700 hover:bg-gray-700">

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))
   }
 }

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,
   ]),
 ])();

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())});