diff --git a/client/src/App.tsx b/client/src/App.tsx index 25eea40d..6c3c0705 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -7,6 +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 CodeMirror, { EditorView } from '@uiw/react-codemirror' @@ -26,6 +27,7 @@ interface UrlArgs { project: string | null url: string | null code: string | null + codez: string | null } /** @@ -286,7 +288,11 @@ function App() { if (args.code) { let _code = decodeURIComponent(args.code) setContent(_code) + } else if (args.codez) { + let _code = LZString.decompressFromBase64(args.codez); + setContent(_code); } + if (args.url) {setUrl(decodeURIComponent(args.url))} if (args.project && args.project != project) { console.log(`[Lean4web] setting project to ${args.project}`) @@ -320,18 +326,24 @@ function App() { let _project = (project == 'mathlib-demo' ? null : project) if (code === contentFromUrl) { if (url !== null) { - let args = {project: _project, url: encodeURIComponent(url), code: null} + let args = {project: _project, url: encodeURIComponent(url), code: null, codez: null} history.replaceState(undefined, undefined!, formatArgs(args)) } else { - let args = {project: _project, url: null, code: null} + let args = {project: _project, url: null, code: null, codez: null} history.replaceState(undefined, undefined!, formatArgs(args)) } } else if (code === "") { - let args = {project: _project, url: null, code: null} + let args = {project: _project, url: null, code: null, codez: null} history.replaceState(undefined, undefined!, formatArgs(args)) } else { - let args = {project: _project, url: null, code: fixedEncodeURIComponent(code)} - history.replaceState(undefined, undefined!, formatArgs(args)) + const compressed = LZString.compressToBase64(code).replace(/=*$/, ''); + 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)) + } } }, [editor, project, code, contentFromUrl]) diff --git a/package-lock.json b/package-lock.json index 692b6df4..1f16aecc 100644 --- a/package-lock.json +++ b/package-lock.json @@ -14,12 +14,14 @@ "@fortawesome/react-fontawesome": "^0.2.2", "@mui/material": "^5.16.4", "@types/file-saver": "^2.0.7", + "@types/lz-string": "^1.5.0", "@uiw/react-codemirror": "^4.23.0", "concurrently": "^8.2.2", "express": "^4.19.2", "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", "lean4monaco": "^1.0.24", + "lz-string": "^1.5.0", "memfs": "^4.11.1", "nocache": "^4.0.0", "node": "^22.6.0", @@ -2530,6 +2532,15 @@ "resolved": "https://registry.npmjs.org/@types/file-saver/-/file-saver-2.0.7.tgz", "integrity": "sha512-dNKVfHd/jk0SkR/exKGj2ggkB45MAkzvWCaqLUUgkyjITkGNzH8H+yUwr+BLJUBjZOe9w8X3wgmXhZDRg1ED6A==" }, + "node_modules/@types/lz-string": { + "version": "1.5.0", + "resolved": "https://registry.npmjs.org/@types/lz-string/-/lz-string-1.5.0.tgz", + "integrity": "sha512-s84fKOrzqqNCAPljhVyC5TjAo6BH4jKHw9NRNFNiRUY5QSgZCmVm5XILlWbisiKl+0OcS7eWihmKGS5akc2iQw==", + "deprecated": "This is a stub types definition. lz-string provides its own type definitions, so you do not need this installed.", + "dependencies": { + "lz-string": "*" + } + }, "node_modules/@types/node": { "version": "22.1.0", "resolved": "https://registry.npmjs.org/@types/node/-/node-22.1.0.tgz", @@ -5467,6 +5478,14 @@ "yallist": "^3.0.2" } }, + "node_modules/lz-string": { + "version": "1.5.0", + "resolved": "https://registry.npmjs.org/lz-string/-/lz-string-1.5.0.tgz", + "integrity": "sha512-h5bgJWpxJNswbU7qCrV0tIKQCaS3blPDrqKWx+QxzuzL1zGUzij9XCWLrSLsJPu5t+eWA/ycetzYAO5IOMcWAQ==", + "bin": { + "lz-string": "bin/bin.js" + } + }, "node_modules/magic-string": { "version": "0.30.11", "resolved": "https://registry.npmjs.org/magic-string/-/magic-string-0.30.11.tgz", diff --git a/package.json b/package.json index 53f41ea5..c0a0f960 100644 --- a/package.json +++ b/package.json @@ -25,12 +25,14 @@ "@fortawesome/react-fontawesome": "^0.2.2", "@mui/material": "^5.16.4", "@types/file-saver": "^2.0.7", + "@types/lz-string": "^1.5.0", "@uiw/react-codemirror": "^4.23.0", "concurrently": "^8.2.2", "express": "^4.19.2", "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", "lean4monaco": "^1.0.24", + "lz-string": "^1.5.0", "memfs": "^4.11.1", "nocache": "^4.0.0", "node": "^22.6.0",