add option for word wrapping #10

leanprover-community · Apr 10, 2024 · 5254e28 · 5254e28
1 parent e936b12
commit 5254e28
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 3 deletions.
diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -78,7 +78,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       },
       tabSize: 2,
       'semanticHighlighting.enabled': true,
-      theme: 'vs'
+      theme: 'vs',
+      wordWrap: config.wordWrap
     })
     setEditor(editor)
     const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)
@@ -87,7 +88,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       model.dispose();
       abbrevRewriter.dispose();
     }
-  }, [])
+  }, [config.wordWrap])
 
   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
@@ -23,12 +23,14 @@ 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 [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 _theme = window.localStorage.getItem("theme")
     let _savingAllowed = window.localStorage.getItem("savingAllowed")
     let _customTheme = window.localStorage.getItem("customTheme")
@@ -44,6 +46,10 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
       setTheme(_theme)
       setSavingAllowed(true)
     }
+    if (_wordWrap) {
+      setWordWrap(_wordWrap == "true")
+      setSavingAllowed(true)
+    }
     if (_customTheme) {
       setCustomTheme(_customTheme)
       setSavingAllowed(true)
@@ -64,19 +70,22 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
   useEffect(() => {
     config.abbreviationCharacter = abbreviationCharacter
     config.verticalLayout = verticalLayout
+    config.wordWrap = wordWrap
     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("theme", theme)
       window.localStorage.setItem("customTheme", customTheme)
     } else {
       window.localStorage.removeItem("abbreviationCharacter")
       window.localStorage.removeItem("verticalLayout")
+      window.localStorage.removeItem("wordWrap")
       window.localStorage.removeItem("theme")
       window.localStorage.removeItem("customTheme")
     }
-  }, [savingAllowed, abbreviationCharacter, verticalLayout, theme])
+  }, [savingAllowed, abbreviationCharacter, verticalLayout, wordWrap, theme])
 
   const handleChangeSaving = (ev) => {
     if (ev.target.checked) {
@@ -172,6 +181,10 @@ const Settings: React.FC<{closeNav, theme, setTheme, project, setProject}> =
               <Switch id="verticalLayout" onChange={handleLayoutChange} checked={verticalLayout} />
               <label htmlFor="verticalLayout">Mobile layout (vertical)</label>
             </p>
+            <p>
+              <Switch id="wordWrap" onChange={() => {setWordWrap(!wordWrap)}} checked={wordWrap} />
+              <label htmlFor="wordWrap">Wrap code</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,6 +7,7 @@ export const config = {
   'inputModeCustomTranslations': {},
   'eagerReplacementEnabled': true,
   'verticalLayout': false, // value here irrelevant, will be overwritten with `width < 800` in Settings.tsx
+  'wordWrap': false,
   'theme': 'lightPlus',
   'customTheme': '',
 }