add acceptSuggestionOnEnter to settings

leanprover-community · May 24, 2024 · 1ed09cf · 1ed09cf
1 parent 295261a
commit 1ed09cf
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 5 deletions.
diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -89,9 +89,9 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       'semanticHighlighting.enabled': true,
       theme: 'vs',
       wordWrap: config.wordWrap ? "on" : "off",
+      acceptSuggestionOnEnter: config.acceptSuggestionOnEnter ? "on" : "off",
       fontFamily: "JuliaMono",
       wrappingStrategy: "advanced",
-      acceptSuggestionOnEnter: "off"
     })
     setEditor(editor)
     const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
@@ -100,7 +100,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       model.dispose();
       abbrevRewriter.dispose();
     }
-  }, [config.wordWrap])
+  }, [config, config.wordWrap, config.acceptSuggestionOnEnter])
 
   useEffect(() => {
     const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" + "/" + project

diff --git a/client/src/Settings.tsx b/client/src/Settings.tsx
@@ -24,14 +24,16 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
     If screen width is below 800, default to vertical layout instead. */
   const {width, height} = useWindowDimensions()
   const [verticalLayout, setVerticalLayout] = React.useState(width < 800)
-  const [wordWrap, setWordWrap] = React.useState(false)
+  const [wordWrap, setWordWrap] = React.useState(true)
+  const [acceptSuggestionOnEnter, setAcceptSuggestionOnEnter] = React.useState(false)
   const [customTheme, setCustomTheme] = React.useState<string>('initial')
 
   // Synchronize state with initial local store
   useEffect(() => {
     let _abbreviationCharacter = window.localStorage.getItem("abbreviationCharacter")
     let _verticalLayout = window.localStorage.getItem("verticalLayout")
     let _wordWrap = window.localStorage.getItem("wordWrap")
+    let _acceptSuggestionOnEnter = window.localStorage.getItem("acceptSuggestionOnEnter")
     let _theme = window.localStorage.getItem("theme")
     let _savingAllowed = window.localStorage.getItem("savingAllowed")
     let _customTheme = window.localStorage.getItem("customTheme")
@@ -51,6 +53,10 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
       setWordWrap(_wordWrap == "true")
       setSavingAllowed(true)
     }
+    if (_acceptSuggestionOnEnter) {
+      setAcceptSuggestionOnEnter(_acceptSuggestionOnEnter == "true")
+      setSavingAllowed(true)
+    }
     if (_customTheme) {
       setCustomTheme(_customTheme)
       setSavingAllowed(true)
@@ -72,21 +78,24 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
     config.abbreviationCharacter = abbreviationCharacter
     config.verticalLayout = verticalLayout
     config.wordWrap = wordWrap
+    config.acceptSuggestionOnEnter = acceptSuggestionOnEnter
     config.theme = theme
     if (savingAllowed) {
       window.localStorage.setItem("abbreviationCharacter", abbreviationCharacter)
       window.localStorage.setItem("verticalLayout", verticalLayout ? 'true' : 'false')
       window.localStorage.setItem("wordWrap", wordWrap ? 'true' : 'false')
+      window.localStorage.setItem("acceptSuggestionOnEnter", acceptSuggestionOnEnter ? 'true' : 'false')
       window.localStorage.setItem("theme", theme)
       window.localStorage.setItem("customTheme", customTheme)
     } else {
       window.localStorage.removeItem("abbreviationCharacter")
       window.localStorage.removeItem("verticalLayout")
       window.localStorage.removeItem("wordWrap")
+      window.localStorage.removeItem("acceptSuggestionOnEnter")
       window.localStorage.removeItem("theme")
       window.localStorage.removeItem("customTheme")
     }
-  }, [savingAllowed, abbreviationCharacter, verticalLayout, wordWrap, theme])
+  }, [savingAllowed, abbreviationCharacter, verticalLayout, wordWrap, acceptSuggestionOnEnter, theme])
 
   const handleChangeSaving = (ev) => {
     if (ev.target.checked) {
@@ -186,6 +195,10 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
               <Switch id="wordWrap" onChange={() => {setWordWrap(!wordWrap)}} checked={wordWrap} />
               <label htmlFor="wordWrap">Wrap code</label>
             </p>
+            <p>
+              <Switch id="acceptSuggestionOnEnter" onChange={() => {setAcceptSuggestionOnEnter(!acceptSuggestionOnEnter)}} checked={acceptSuggestionOnEnter} />
+              <label htmlFor="acceptSuggestionOnEnter">Accept Suggestion on Enter</label>
+            </p>
             <p>
               <Switch id="savingAllowed" onChange={handleChangeSaving} checked={savingAllowed} />
               <label htmlFor="savingAllowed">Save my settings (in the browser store)</label>

diff --git a/client/src/config/config.ts b/client/src/config/config.ts
@@ -7,7 +7,8 @@ export const config = {
   'inputModeCustomTranslations': {},
   'eagerReplacementEnabled': true,
   'verticalLayout': false, // value here irrelevant, will be overwritten with `width < 800` in Settings.tsx
-  'wordWrap': false,
+  'wordWrap': true,
+  'acceptSuggestionOnEnter': false,
   'theme': 'lightPlus',
   'customTheme': '',
 }