add option to disable compression

leanprover-community · Aug 22, 2024 · 9d1b7fe · 9d1b7fe
1 parent 878bbe3
commit 9d1b7fe
Show file tree

Hide file tree

Showing 3 changed files with 18 additions and 5 deletions.
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -7,7 +7,7 @@ import { Menu } from './Navigation'
 import { PreferencesContext } from './Popups/Settings'
 import { useWindowDimensions } from './utils/window_width'
 import LeanLogo from './assets/logo.svg'
-import LZString from 'lz-string';
+import LZString from 'lz-string'
 
 import CodeMirror, { EditorView } from '@uiw/react-codemirror'
 
@@ -289,8 +289,8 @@ function App() {
       let _code = decodeURIComponent(args.code)
       setContent(_code)
     } else if (args.codez) {
-      let _code = LZString.decompressFromBase64(args.codez);
-      setContent(_code);
+      let _code = LZString.decompressFromBase64(args.codez)
+      setContent(_code)
     }
 
     if (args.url) {setUrl(decodeURIComponent(args.url))}
@@ -335,15 +335,21 @@ function App() {
     } else if (code === "") {
       let args = {project: _project, url: null, code: null, codez: null}
       history.replaceState(undefined, undefined!, formatArgs(args))
-    } else {
+    } else if (preferences.compress) {
+      // LZ padds the string with trailing `=`, which mess up the argument parsing
+      // and aren't needed for LZ encoding, so we remove them.
       const compressed = LZString.compressToBase64(code).replace(/=*$/, '');
-      if(compressed.length < code.length) {
+      console.debug(`[Lean4web]: code length: ${code.length}, compressed: ${compressed.length}`)
+      if (compressed.length < code.length) {
         let args = {project: _project, url: null, code: null, codez: compressed}
         history.replaceState(undefined, undefined!, formatArgs(args))
       } else {
         let args = {project: _project, url: null, code: fixedEncodeURIComponent(code), codez: null}
         history.replaceState(undefined, undefined!, formatArgs(args))
       }
+    } else {
+      let args = {project: _project, url: null, code: fixedEncodeURIComponent(code), codez: null}
+      history.replaceState(undefined, undefined!, formatArgs(args))
     }
   }, [editor, project, code, contentFromUrl])
 

diff --git a/client/src/Popups/Settings.tsx b/client/src/Popups/Settings.tsx
@@ -104,6 +104,11 @@ const SettingsPopup: FC<{
         />
         <label htmlFor="mobile">Mobile layout (vertical)</label>
       </p>
+      <p>
+        <Switch id="compress" onChange={() => {modifyPreferences("compress", !preferences.compress)}}
+        checked={preferences.compress} />
+        <label htmlFor="compress">Compress code in URL (if shorter)</label>
+      </p>
       <p>
         <Switch id="wordWrap" onChange={() => {modifyPreferences("wordWrap", !preferences.wordWrap)}}
         checked={preferences.wordWrap} />

diff --git a/client/src/config/settings.ts b/client/src/config/settings.ts
@@ -10,6 +10,7 @@ Note that more Editor options are set in `App.tsx` directly.
 export interface IPreferencesContext {
   abbreviationCharacter: string
   acceptSuggestionOnEnter: boolean
+  compress: boolean, // compress the `code=` in the URL into `codez=` using LZ-string
   mobile: boolean
   saveInLocalStore: boolean
   theme: string,
@@ -20,6 +21,7 @@ export interface IPreferencesContext {
 const settings: IPreferencesContext = {
   abbreviationCharacter: '\\',
   acceptSuggestionOnEnter: false,
+  compress: true,
   mobile: false, // value irrelevant as it will be overwritten with `width < 800` in App.tsx
   saveInLocalStore: false, // should be false unless user gave consent.
   theme: 'Visual Studio Light', // irrelevant as it will be overwritten in App.tsx