fix Ctrl+Enter default behavior

This commit is contained in:
2023-08-22 13:23:17 +02:00
parent 09b3ad3fc0
commit f2ba2d05f6

View File

@ -1,9 +1,9 @@
import { EditorState, Compartment } from "@codemirror/state";
import { ViewUpdate, lineNumbers } from "@codemirror/view";
import { ViewUpdate, lineNumbers, keymap } from "@codemirror/view";
import { javascript } from "@codemirror/lang-javascript";
import { oneDark } from "@codemirror/theme-one-dark";
import { markdown } from "@codemirror/lang-markdown";
import { Extension } from "@codemirror/state";
import { Extension, Prec } from "@codemirror/state";
import { vim } from "@replit/codemirror-vim";
import { AppSettings } from "./AppSettings";
import { editorSetup } from "./EditorSetup";
@ -102,9 +102,9 @@ export class Editor {
documentation_button: HTMLButtonElement = document.getElementById(
"doc-button-1"
) as HTMLButtonElement;
eval_button: HTMLButtonElement = document.getElementById(
"eval-button-1"
) as HTMLButtonElement;
eval_button: HTMLButtonElement = document.getElementById(
"eval-button-1"
) as HTMLButtonElement;
// Script selection elements
local_button: HTMLButtonElement = document.getElementById(
@ -164,9 +164,11 @@ export class Editor {
) as HTMLButtonElement;
// Error line
error_line: HTMLElement = document.getElementById("error_line") as HTMLElement
show_error: boolean = false
error_line: HTMLElement = document.getElementById(
"error_line"
) as HTMLElement;
show_error: boolean = false;
constructor() {
// ================================================================================
// Loading the universe from local storage
@ -226,6 +228,9 @@ export class Editor {
...this.editorExtensions,
EditorView.lineWrapping,
dynamicPlugins.of(this.userPlugins),
Prec.highest(keymap.of([
{ key:"Ctrl-Enter", run: ()=>{return true} }
])),
],
doc: this.universes[this.selected_universe].locals[this.local_index]
.candidate,
@ -527,17 +532,16 @@ export class Editor {
"about",
].forEach((e) => {
let name = `docs_` + e;
document.getElementById(name)!
.addEventListener("click", () => {
this.currentDocumentationPane = e;
this.updateDocumentationContent();
});
});
document.getElementById(name)!.addEventListener("click", () => {
this.currentDocumentationPane = e;
this.updateDocumentationContent();
});
});
// Passing the API to the User
Object.entries(this.api).forEach(([name, value]) => {
(globalThis as Record<string, any>)[name] = value;
});
// Passing the API to the User
Object.entries(this.api).forEach(([name, value]) => {
(globalThis as Record<string, any>)[name] = value;
});
}
get note_buffer() {