From 0f8f327a11e5aaca957abdde32a91348a8961d01 Mon Sep 17 00:00:00 2001 From: Raphael Forment Date: Fri, 25 Aug 2023 08:30:33 +0200 Subject: [PATCH] boot topos in global mode --- src/main.ts | 55 ++++++++++++++++++++++++++++------------------------- 1 file changed, 29 insertions(+), 26 deletions(-) diff --git a/src/main.ts b/src/main.ts index 7156ca5..0ce5cf9 100644 --- a/src/main.ts +++ b/src/main.ts @@ -66,7 +66,7 @@ export class Editor { universes: Universes = template_universes; selected_universe: string; local_index: number = 1; - editor_mode: "global" | "local" | "init" | "notes" = "local"; + editor_mode: "global" | "local" | "init" | "notes" = "global"; fontSize: Compartment; withLineNumbers: Compartment; vimModeCompartment: Compartment; @@ -235,31 +235,6 @@ export class Editor { ]; let dynamicPlugins = new Compartment(); - this.state = EditorState.create({ - extensions: [ - ...this.editorExtensions, - EditorView.lineWrapping, - dynamicPlugins.of(this.userPlugins), - Prec.highest( - keymap.of([ - { - key: "Ctrl-Enter", - run: () => { - return true; - }, - }, - ]) - ), - keymap.of([indentWithTab]), - ], - doc: this.universes[this.selected_universe].locals[this.local_index] - .candidate, - }); - - this.view = new EditorView({ - parent: document.getElementById("editor") as HTMLElement, - state: this.state, - }); // ================================================================================ // Application event listeners @@ -595,6 +570,34 @@ export class Editor { } } } + + this.state = EditorState.create({ + extensions: [ + ...this.editorExtensions, + EditorView.lineWrapping, + dynamicPlugins.of(this.userPlugins), + Prec.highest( + keymap.of([ + { + key: "Ctrl-Enter", + run: () => { + return true; + }, + }, + ]) + ), + keymap.of([indentWithTab]), + ], + doc: this.universes[this.selected_universe].global.candidate, + }); + + this.view = new EditorView({ + parent: document.getElementById("editor") as HTMLElement, + state: this.state, + }); + + this.changeModeFromInterface("global"); + } get note_buffer() {