disable accepting suggestions on enter

leanprover-community · May 24, 2024 · 295261a · 295261a
1 parent 52dcd80
commit 295261a
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -65,6 +65,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
     if (onDidChangeContent) {
       model.onDidChangeContent(() => onDidChangeContent(model.getValue()))
     }
+    // see available options here:
+    // https://microsoft.github.io/monaco-editor/typedoc/variables/editor.EditorOptions.html
     const editor = monaco.editor.create(codeviewRef.current!, {
       model,
       glyphMargin: true,
@@ -88,7 +90,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       theme: 'vs',
       wordWrap: config.wordWrap ? "on" : "off",
       fontFamily: "JuliaMono",
-      wrappingStrategy: "advanced"
+      wrappingStrategy: "advanced",
+      acceptSuggestionOnEnter: "off"
     })
     setEditor(editor)
     const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)