diff --git a/.eslintrc.cjs b/.eslintrc.cjs deleted file mode 100644 index 6e8698b7..00000000 --- a/.eslintrc.cjs +++ /dev/null @@ -1,18 +0,0 @@ -module.exports = { - root: true, - env: { browser: true, es2020: true }, - extends: [ - "eslint:recommended", - "plugin:@typescript-eslint/recommended", - "plugin:react-hooks/recommended", - ], - ignorePatterns: ["dist", ".eslintrc.cjs"], - parser: "@typescript-eslint/parser", - plugins: ["react-refresh"], - rules: { - "react-refresh/only-export-components": [ - "warn", - { allowConstantExport: true }, - ], - }, -}; diff --git a/.github/workflows/build.yml b/.github/workflows/ci.yml similarity index 90% rename from .github/workflows/build.yml rename to .github/workflows/ci.yml index a041f5c9..98b14dee 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/ci.yml @@ -1,5 +1,5 @@ -name: Test -run-name: test +name: CI +run-name: ci on: workflow_dispatch: push: @@ -7,15 +7,14 @@ on: - "main" - "dev" pull_request: - concurrency: group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }} cancel-in-progress: true - defaults: run: shell: bash - +env: + NODE_VERSION: 25 jobs: test: runs-on: ${{ matrix.os }} @@ -34,7 +33,7 @@ jobs: - name: Setup Node.js uses: actions/setup-node@v4 with: - node-version: "25" + node-version: ${{ env.NODE_VERSION }} - name: Install elan uses: leanprover/lean-action@v1 @@ -132,7 +131,20 @@ jobs: with: name: cypress-screenshots-production-windows-${{ matrix.os }}-${{ matrix.browser }} path: cypress/screenshots - + lint: + name: Lint + runs-on: ubuntu-latest + steps: + - name: Checkout repository + uses: actions/checkout@v4 + - name: Setup Node.js + uses: actions/setup-node@v4 + with: + node-version: ${{ env.NODE_VERSION }} + - name: Install dependencies + run: npm ci + - name: lint + run: npm run lint all-tests-pass: name: All Tests Pass runs-on: ubuntu-latest diff --git a/.vscode/settings.json b/.vscode/settings.json index d1b4edb2..5dcf9686 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -1,4 +1,15 @@ { "editor.formatOnSave": true, - "editor.defaultFormatter": "esbenp.prettier-vscode" -} \ No newline at end of file + "editor.defaultFormatter": "esbenp.prettier-vscode", + "eslint.enable": true, + "eslint.validate": [ + "javascript", + "javascriptreact", + "typescript", + "typescriptreact" + ], + "eslint.workingDirectories": [{ "mode": "auto" }], + "editor.codeActionsOnSave": { + "source.fixAll.eslint": "explicit" + } +} diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json index 5c3d298e..ca7adbd5 100644 --- a/Projects/MathlibDemo/lake-manifest.json +++ b/Projects/MathlibDemo/lake-manifest.json @@ -1,116 +1,95 @@ -{ - "version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": [ - { - "url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "d68c4dc09f5e000d3c968adae8def120a0758729", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "ef8377f31b5535430b6753a974d685b0019d0681", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.84", - "inherited": true, - "configFile": "lakefile.lean" - }, - { - "url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml" - }, - { - "url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.27.0-rc1", - "inherited": true, - "configFile": "lakefile.toml" - } - ], - "name": "MathlibDemo", - "lakeDir": ".lake" -} +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": + [{"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "63710499c7ac0bd4ab1977494d82e3017ac59edf", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b3dd6c3ebc0a71685e86bea9223be39ea4c299fb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5ce7f0a355f522a952a3d678d696bd563bb4fd28", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "cff9dd30f2c161b9efd7c657cafed1f967645890", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ef8377f31b5535430b6753a974d685b0019d0681", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.84", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "fa78cf032194308a950a264ed87b422a2a7c1c6c", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "8920dcbb96a4e8bf641fc399ac9c0888e4a6be72", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2e16f91af2a97975e5d2fac906494cd6c17ba255", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.27.0-rc1", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "MathlibDemo", + "lakeDir": ".lake"} diff --git a/Projects/Stable/lake-manifest.json b/Projects/Stable/lake-manifest.json index 1d38c03d..19497751 100644 --- a/Projects/Stable/lake-manifest.json +++ b/Projects/Stable/lake-manifest.json @@ -1,7 +1,5 @@ -{ - "version": "1.1.0", - "packagesDir": ".lake/packages", - "packages": [], - "name": "Stable", - "lakeDir": ".lake" -} +{"version": "1.1.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "Stable", + "lakeDir": ".lake"} diff --git a/client/src/.prettierrc.json b/client/src/.prettierrc.json index 70ae7996..7ef6ab72 100644 --- a/client/src/.prettierrc.json +++ b/client/src/.prettierrc.json @@ -2,7 +2,7 @@ "printWidth": 100, "tabWidth": 2, "useTabs": false, - "semi": true, + "semi": false, "singleQuote": true, "quoteProps": "as-needed", "jsxSingleQuote": false, diff --git a/client/src/App.tsx b/client/src/App.tsx index 01bcd32f..333a3cbf 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,107 +1,83 @@ -import { useCallback, useEffect, useRef, useState } from 'react'; -import Split from 'react-split'; -import * as monaco from 'monaco-editor'; -import CodeMirror, { EditorView } from '@uiw/react-codemirror'; -import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco'; -import LZString from 'lz-string'; -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'; -import { faCode } from '@fortawesome/free-solid-svg-icons'; -import * as path from 'path'; -import { mobileAtom, settingsAtom, settingsUrlAtom } from './settings/settings-atoms'; -import { useAtom } from 'jotai/react'; -import { screenWidthAtom } from './store/window-atoms'; -import LeanLogo from './assets/logo.svg'; -import { lightThemes } from './settings/settings-types'; -import { Menu } from './Navigation'; -import { save } from './utils/SaveToFile'; -import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing'; -import './css/App.css'; -import './css/Editor.css'; +import './css/App.css' +import './css/Editor.css' + +import { faCode } from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import CodeMirror, { EditorView } from '@uiw/react-codemirror' +import { useAtom } from 'jotai/react' +import { LeanMonaco, LeanMonacoEditor, LeanMonacoOptions } from 'lean4monaco' +import * as monaco from 'monaco-editor' +import * as path from 'path' +import { useCallback, useEffect, useRef, useState } from 'react' +import Split from 'react-split' + +import LeanLogo from './assets/logo.svg' +import { codeAtom } from './editor/code-atoms' +import { Menu } from './navigation/Navigation' +import { mobileAtom, settingsAtom } from './settings/settings-atoms' +import { lightThemes } from './settings/settings-types' +import { freshlyImportedCodeAtom } from './store/import-atoms' +import { projectAtom } from './store/project-atoms' +import { screenWidthAtom } from './store/window-atoms' +import { save } from './utils/SaveToFile' /** Returns true if the browser wants dark mode */ function isBrowserDefaultDark() { - return window.matchMedia('(prefers-color-scheme: dark)').matches; + return window.matchMedia('(prefers-color-scheme: dark)').matches } function App() { - const editorRef = useRef(null); - const infoviewRef = useRef(null); - const [dragging, setDragging] = useState(false); - const [editor, setEditor] = useState(); - const [leanMonaco, setLeanMonaco] = useState(); - const [settings] = useAtom(settingsAtom); - const [mobile] = useAtom(mobileAtom); - const [, setScreenWidth] = useAtom(screenWidthAtom); - const [searchParams] = useAtom(settingsUrlAtom); + const editorRef = useRef(null) + const infoviewRef = useRef(null) + const [dragging, setDragging] = useState(false) + const [editor, setEditor] = useState() + const [leanMonaco, setLeanMonaco] = useState() + const [settings] = useAtom(settingsAtom) + const [mobile] = useAtom(mobileAtom) + const [, setScreenWidth] = useAtom(screenWidthAtom) + const [project] = useAtom(projectAtom) + const [code, setCode] = useAtom(codeAtom) + const [freshlyImportedCode] = useAtom(freshlyImportedCodeAtom) + + const model = editor?.getModel() // Lean4monaco options const [options, setOptions] = useState({ // placeholder, updated below websocket: { url: '' }, - }); + }) // Because of Monaco's missing mobile support we add a codeMirror editor // which can be enabled to do editing. // TODO: It would be nice to integrate Lean into CodeMirror better. // first step could be to pass the cursor selection to the underlying monaco editor - const [codeMirror, setCodeMirror] = useState(false); - - // the user data - const [code, setCode] = useState(''); - const [project, setProject] = useState('MathlibDemo'); - const [url, setUrl] = useState(null); - const [codeFromUrl, setCodeFromUrl] = useState(''); + const [codeMirror, setCodeMirror] = useState(false) /** Monaco editor requires the code to be set manually. */ - function setContent(code: string) { - editor?.getModel()?.setValue(code); - setCode(code); + function setContent(_code: string) { + editor?.getModel()?.setValue(_code) + setCode(_code) } - // Read the URL arguments - useEffect(() => { - // Parse args - console.log('[Lean4web] Parsing URL'); - let args = parseArgs(); - 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(lookupUrl(decodeURIComponent(args.url))); - } - - // if no project provided, use default - let project = args.project ?? 'MathlibDemo'; - - console.log(`[Lean4web] Setting project to ${project}`); - setProject(project); - }, []); - // save the screen width in jotai useEffect(() => { - const handleResize = () => setScreenWidth(window.innerWidth); - window.addEventListener('resize', handleResize); - return () => window.removeEventListener('resize', handleResize); - }, [setScreenWidth]); + const handleResize = () => setScreenWidth(window.innerWidth) + window.addEventListener('resize', handleResize) + return () => window.removeEventListener('resize', handleResize) + }, [setScreenWidth]) // Update LeanMonaco options when preferences are loaded or change useEffect(() => { - if (!project) { - return; - } - console.log('[Lean4web] Update lean4monaco options'); + if (!project) return + + console.log('[Lean4web] Update lean4monaco options') var socketUrl = (window.location.protocol === 'https:' ? 'wss://' : 'ws://') + window.location.host + '/websocket/' + - project; - console.log(`[Lean4web] Socket url is ${socketUrl}`); + project + console.log(`[Lean4web] Socket url is ${socketUrl}`) var _options: LeanMonacoOptions = { websocket: { url: socketUrl }, // Restrict monaco's extend (e.g. context menu) to the editor itself @@ -126,28 +102,28 @@ function App() { 'lean4.infoview.showTooltipOnHover': false, 'lean4.input.leader': settings.abbreviationCharacter, }, - }; - setOptions(_options); - }, [editorRef, project, settings]); + } + setOptions(_options) + }, [editorRef, project, settings]) // Setting up the editor and infoview useEffect(() => { - if (project === undefined) return; - console.debug('[Lean4web] Restarting editor'); - var _leanMonaco = new LeanMonaco(); - var leanMonacoEditor = new LeanMonacoEditor(); + if (project === undefined) return + console.debug('[Lean4web] Restarting editor') + var _leanMonaco = new LeanMonaco() + var leanMonacoEditor = new LeanMonacoEditor() - _leanMonaco.setInfoviewElement(infoviewRef.current!); - (async () => { - await _leanMonaco.start(options); + _leanMonaco.setInfoviewElement(infoviewRef.current!) + ;(async () => { + await _leanMonaco.start(options) await leanMonacoEditor.start( editorRef.current!, path.join(project, `${project}.lean`), code ?? '', - ); + ) - setEditor(leanMonacoEditor.editor); - setLeanMonaco(_leanMonaco); + setEditor(leanMonacoEditor.editor) + setLeanMonaco(_leanMonaco) // Add a `Paste` option to the context menu on mobile. // Monaco does not support clipboard pasting as all browsers block it @@ -160,9 +136,9 @@ function App() { // keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V], contextMenuGroupId: '9_cutcopypaste', run: (_editor) => { - setCodeMirror(true); + setCodeMirror(true) }, - }); + }) } // // TODO: This was an approach to create a new definition provider, but it @@ -188,11 +164,11 @@ function App() { // TODO: Implement Go-To-Definition better // This approach only gives us the file on the server (plus line number) it wants // to open, is there a better approach? - const editorService = (leanMonacoEditor.editor as any)?._codeEditorService; + const editorService = (leanMonacoEditor.editor as any)?._codeEditorService if (editorService) { - const openEditorBase = editorService.openCodeEditor.bind(editorService); + const openEditorBase = editorService.openCodeEditor.bind(editorService) editorService.openCodeEditor = async (input: any, source: any) => { - const result = await openEditorBase(input, source); + const result = await openEditorBase(input, source) if (result === null) { // found this out with `console.debug(input)`: // `resource.path` is the file go-to-def tries to open on the disk @@ -201,7 +177,7 @@ function App() { // call `...${path}.html#${declaration}` let path = input.resource.path .replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '') - .replace(new RegExp('\.lean$'), ''); + .replace(new RegExp('\.lean$'), '') if ( window.confirm( @@ -211,174 +187,84 @@ function App() { let newTab = window.open( `https://leanprover-community.github.io/mathlib4_docs/${path}.html`, '_blank', - ); + ) if (newTab) { - newTab.focus(); + newTab.focus() } } } - return null; + return null // return result // always return the base result - }; + } } // Keeping the `code` state up-to-date with the changes in the editor leanMonacoEditor.editor?.onDidChangeModelContent(() => { - setCode(leanMonacoEditor.editor?.getModel()?.getValue()!); - }); - })(); - return () => { - leanMonacoEditor.dispose(); - _leanMonaco.dispose(); - }; - }, [project, settings, options, infoviewRef, editorRef]); - - // Load content from source URL. - // Once the editor is loaded, this reads the content of any provided `url=` in the URL and - // saves this content as `codeFromURL`. It is important that we only do this once - // the editor is loaded, as the `useEffect` below only triggers when the `codeFromURL` - // changes, otherwise it might overwrite local changes too often. - useEffect(() => { - if (!editor || !url) { - return; - } - console.debug(`[Lean4web] Loading from ${url}`); - fetch(url) - .then((response) => response.text()) - .then((code) => { - setCodeFromUrl(code); + setCode(leanMonacoEditor.editor?.getModel()?.getValue()!) }) - .catch((err) => { - let errorTxt = `ERROR: ${err.toString()}`; - console.error(errorTxt); - setCodeFromUrl(errorTxt); - }); - }, [url, editor]); - - // Sets the editors content to the content from the loaded URL. - // As described above, this requires the editor is loaded, but we do not want to - // trigger this effect every time the editor is reloaded (e.g. config change) as otherwise - // we would constantly overwrite the user's local changes - useEffect(() => { - if (!codeFromUrl) { - return; + })() + return () => { + leanMonacoEditor.dispose() + _leanMonaco.dispose() } - setContent(codeFromUrl); - }, [codeFromUrl]); + }, [infoviewRef, editorRef, options, project, settings]) - // Keep the URL updated on change + /** Set editor content to the code loaded from the URL */ useEffect(() => { - if (!editor) { - return; - } - - let _project = project == 'MathlibDemo' ? null : (project ?? null); - let args: { - project: string | null; - url: string | null; - code: string | null; - codez: string | null; - }; - if (code === '') { - args = { - project: _project, - url: null, - code: null, - codez: null, - }; - } else if (url != null && code == codeFromUrl) { - args = { - project: _project, - url: encodeURIComponent(url), - code: null, - codez: null, - }; - } else if (settings.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(/=*$/, ''); - // // Note: probably temporary; might be worth to always compress as with whitespace encoding - // // it needs very little for the compressed version to be shorter - // const encodedCode = fixedEncodeURIComponent(code) - // console.debug(`[Lean4web] Code length: ${encodedCode.length}, compressed: ${compressed.length}`) - // if (compressed.length < encodedCode.length) { - args = { - project: _project, - url: null, - code: null, - codez: compressed, - }; - // } else { - // args = { - // project: _project, - // url: null, - // code: encodedCode, - // codez: null - // } - // } - } else { - args = { - project: _project, - url: null, - code: fixedEncodeURIComponent(code), - codez: null, - }; - } - history.replaceState(undefined, undefined!, formatArgs(args)); - }, [editor, project, code, codeFromUrl]); + if (freshlyImportedCode && model) model.setValue(freshlyImportedCode) + }, [freshlyImportedCode, model]) // Disable monaco context menu outside the editor useEffect(() => { const handleContextMenu = (event: MouseEvent) => { - const editorContainer = document.querySelector('.editor'); + const editorContainer = document.querySelector('.editor') if (editorContainer && !editorContainer.contains(event.target as Node)) { - event.stopPropagation(); + event.stopPropagation() } - }; - document.addEventListener('contextmenu', handleContextMenu, true); + } + document.addEventListener('contextmenu', handleContextMenu, true) return () => { - document.removeEventListener('contextmenu', handleContextMenu, true); - }; - }, []); + document.removeEventListener('contextmenu', handleContextMenu, true) + } + }, []) // Stop the browser's save dialog on Ctrl+S const handleKeyDown = useCallback((event: KeyboardEvent) => { if ((event.ctrlKey || event.metaKey) && event.key.toLowerCase() === 's') { - event.preventDefault(); + event.preventDefault() } - }, []); + }, []) // Actually save the file on Ctrl+S const handleKeyUp = useCallback( (event: KeyboardEvent) => { - if ((event.ctrlKey || event.metaKey) && event.key.toLowerCase() === 's') { - event.preventDefault(); - save(code); + if ( + (event.ctrlKey || event.metaKey) && + event.key.toLowerCase() === 's' && + code !== undefined + ) { + event.preventDefault() + save(code) } }, [code], - ); + ) useEffect(() => { - document.addEventListener('keydown', handleKeyDown); - document.addEventListener('keyup', handleKeyUp); + document.addEventListener('keydown', handleKeyDown) + document.addEventListener('keyup', handleKeyUp) return () => { - document.removeEventListener('keydown', handleKeyDown); - document.removeEventListener('keyup', handleKeyUp); - }; - }, [handleKeyDown, handleKeyUp]); + document.removeEventListener('keydown', handleKeyDown) + document.removeEventListener('keyup', handleKeyUp) + } + }, [handleKeyDown, handleKeyUp]) return (
- ); + ) } -export default App; +export default App diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx deleted file mode 100644 index d9dc59bd..00000000 --- a/client/src/Navigation.tsx +++ /dev/null @@ -1,411 +0,0 @@ -import { - ChangeEvent, - Dispatch, - FC, - JSX, - MouseEventHandler, - ReactNode, - SetStateAction, - useState, -} from 'react'; -import { FontAwesomeIcon } from '@fortawesome/react-fontawesome'; -import { - IconDefinition, - faArrowRotateRight, - faCode, - faInfoCircle, -} from '@fortawesome/free-solid-svg-icons'; -import ZulipIcon from './assets/zulip.svg'; -import { - faArrowUpRightFromSquare, - faDownload, - faBars, - faXmark, - faShield, - faHammer, - faGear, - faStar, - faUpload, - faCloudArrowUp, -} from '@fortawesome/free-solid-svg-icons'; - -import PrivacyPopup from './Popups/PrivacyPolicy'; -import ImpressumPopup from './Popups/Impressum'; -import ToolsPopup from './Popups/Tools'; -import LoadUrlPopup from './Popups/LoadUrl'; -import LoadZulipPopup from './Popups/LoadZulip'; - -import lean4webConfig from './config/config'; -import './css/Modal.css'; -import './css/Navigation.css'; -import { save } from './utils/SaveToFile'; -import { lookupUrl } from './utils/UrlParsing'; -import { mobileAtom } from './settings/settings-atoms'; -import { useAtom } from 'jotai'; -import { SettingsPopup } from './settings/SettingsPopup'; - -/** A button to appear in the hamburger menu or to navigation bar. */ -export const NavButton: FC<{ - icon?: IconDefinition; - iconElement?: JSX.Element; - text: string; - onClick?: MouseEventHandler; - href?: string; -}> = ({ icon, iconElement, text, onClick = () => {}, href = null }) => { - // note: it seems that we can just leave the `target="_blank"` and it has no - // effect on links without a `href`. If not, add `if (href)` statement here... - return ( - - {iconElement ?? } {text} - - ); -}; - -/** A button to appear in the hamburger menu or to navigation bar. */ -export const Dropdown: FC<{ - open: boolean; - setOpen: Dispatch>; - icon?: IconDefinition; - text?: string; - useOverlay?: boolean; - onClick?: MouseEventHandler; - children?: ReactNode; -}> = ({ open, setOpen, icon, text, useOverlay = false, onClick, children }) => { - return ( - <> -
- { - setOpen(!open); - onClick!(ev); - ev.stopPropagation(); - }} - /> - {open && ( -
setOpen(false)}> - {children} -
- )} -
- {useOverlay && open && ( -
{ - setOpen(false); - ev.stopPropagation(); - }} - /> - )} - - ); -}; - -/** A popup which overlays the entire screen. */ -export const Popup: FC<{ - open: boolean; - handleClose: () => void; // TODO: what's the correct type? - children?: ReactNode; -}> = ({ open, handleClose, children }) => { - return ( -
-
-
-
- {children} -
-
- ); -}; - -/** The menu items either appearing inside the dropdown or outside */ -const FlexibleMenu: FC<{ - isInDropdown: boolean; - setOpenNav: Dispatch>; - openExample: boolean; - setOpenExample: Dispatch>; - openLoad: boolean; - setOpenLoad: Dispatch>; - loadFromUrl: (url: string, project?: string | undefined) => void; - setContent: (code: string) => void; - setLoadUrlOpen: Dispatch>; - setLoadZulipOpen: Dispatch>; -}> = ({ - isInDropdown = false, - setOpenNav, - openExample, - setOpenExample, - openLoad, - setOpenLoad, - loadFromUrl, - setContent, - setLoadUrlOpen, - setLoadZulipOpen, -}) => { - const loadFileFromDisk = (event: ChangeEvent) => { - console.debug('Loading file from disk'); - const fileToLoad = event.target.files![0]; - var fileReader = new FileReader(); - fileReader.onload = (fileLoadedEvent) => { - var textFromFileLoaded = fileLoadedEvent.target!.result as string; - setContent(textFromFileLoaded); - }; - fileReader.readAsText(fileToLoad, 'UTF-8'); - // Manually close the menu as we prevent it closing below. - setOpenLoad(false); - }; - - return ( - <> - { - setOpenLoad(false); - !isInDropdown && setOpenNav(false); - }} - > - {lean4webConfig.projects.map((proj) => - proj.examples?.map((example) => ( - { - loadFromUrl( - `${window.location.origin}/api/example/${proj.folder}/${example.file}`, - proj.folder, - ); - setOpenExample(false); - }} - /> - )), - )} - - { - setOpenExample(false); - !isInDropdown && setOpenNav(false); - }} - > - ev.stopPropagation()} - /> - {/* Need `ev.stopPropagation` to prevent closing until the file is loaded. - Otherwise the file-upload is destroyed too early. */} - - { - setLoadUrlOpen(true); - }} - /> - } - text="Load Zulip Message" - onClick={() => { - setLoadZulipOpen(true); - }} - /> - - - ); -}; - -/** The Navigation menu */ -export const Menu: FC<{ - code: string; - setContent: (code: string) => void; - project: string; - setProject: Dispatch>; - setUrl: Dispatch>; - codeFromUrl: string; - restart?: () => void; - codeMirror: boolean; - setCodeMirror: Dispatch>; -}> = ({ - code, - setContent, - project, - setProject, - setUrl, - codeFromUrl, - restart, - codeMirror, - setCodeMirror, -}) => { - // state for handling the dropdown menus - const [openNav, setOpenNav] = useState(false); - const [openExample, setOpenExample] = useState(false); - const [openLoad, setOpenLoad] = useState(false); - const [loadUrlOpen, setLoadUrlOpen] = useState(false); - const [loadZulipOpen, setLoadZulipOpen] = useState(false); - - // state for the popups - const [privacyOpen, setPrivacyOpen] = useState(false); - const [impressumOpen, setImpressumOpen] = useState(false); - const [toolsOpen, setToolsOpen] = useState(false); - const [settingsOpen, setSettingsOpen] = useState(false); - - const [mobile] = useAtom(mobileAtom); - - const loadFromUrl = (url: string, project: string | undefined = undefined) => { - url = lookupUrl(url); - console.debug('load code from url'); - setUrl((oldUrl: string | null) => { - if (oldUrl === url) { - setContent(codeFromUrl); - } - return url; - }); - if (project) { - setProject(project); - } - }; - - const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails; - - return ( -
- - {mobile && ( - { - setCodeMirror(!codeMirror); - }} - /> - )} - {!mobile && ( - - )} - { - setOpenExample(false); - setOpenLoad(false); - }} - > - {mobile && ( - - )} - { - setSettingsOpen(true); - }} - /> - setToolsOpen(true)} /> - - save(code)} /> - { - setPrivacyOpen(true); - }} - /> - {hasImpressum && ( - { - setImpressumOpen(true); - }} - /> - )} - - - - - setPrivacyOpen(false)} /> - {hasImpressum && ( - setImpressumOpen(false)} /> - )} - setToolsOpen(false)} project={project} /> - setSettingsOpen(false)} - closeNav={() => setOpenNav(false)} - project={project} - setProject={setProject} - /> - setLoadUrlOpen(false)} - loadFromUrl={loadFromUrl} - /> - setLoadZulipOpen(false)} - setContent={setContent} - /> -
- ); -}; diff --git a/client/src/Popups/Impressum.tsx b/client/src/Popups/Impressum.tsx index 00203ed9..887471ec 100644 --- a/client/src/Popups/Impressum.tsx +++ b/client/src/Popups/Impressum.tsx @@ -1,12 +1,8 @@ -import { FC } from 'react'; -import { Popup } from '../Navigation'; -import lean4webConfig from '../config/config'; +import lean4webConfig from '../config/config' +import { Popup } from '../navigation/Popup' /** The popup with the privacy policy. */ -const ImpressumPopup: FC<{ - open: boolean; - handleClose: () => void; -}> = ({ open, handleClose }) => { +function ImpressumPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) { return (

Impressum

@@ -21,7 +17,7 @@ const ImpressumPopup: FC<{ {lean4webConfig.impressum} - ); -}; + ) +} -export default ImpressumPopup; +export default ImpressumPopup diff --git a/client/src/Popups/LoadUrl.tsx b/client/src/Popups/LoadUrl.tsx index e9c70d6b..f5ac42f0 100644 --- a/client/src/Popups/LoadUrl.tsx +++ b/client/src/Popups/LoadUrl.tsx @@ -1,27 +1,27 @@ -import { Popup } from '../Navigation'; -import { FC, FormEvent, useRef, useState } from 'react'; +import { useAtom } from 'jotai' +import { FormEvent, useRef, useState } from 'react' -const LoadUrlPopup: FC<{ - open: boolean; - handleClose: () => void; - loadFromUrl: (url: string) => void; -}> = ({ open, handleClose, loadFromUrl }) => { - const [error, setError] = useState(''); - const urlRef = useRef(null); +import { Popup } from '../navigation/Popup' +import { setImportUrlAndProjectAtom } from '../store/import-atoms' + +function LoadUrlPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) { + const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom) + const [error, setError] = useState('') + const urlRef = useRef(null) const handleLoad = (ev: FormEvent) => { - ev.preventDefault(); - let url = urlRef.current?.value; + ev.preventDefault() + let url = urlRef.current?.value if (!url) { - setError(`Please specify a URL.`); - return; + setError(`Please specify a URL.`) + return } if (!url.startsWith('http://') && !url.startsWith('https://')) { - url = 'https://' + url; + url = 'https://' + url } - loadFromUrl(url); - handleClose(); - }; + setImportUrlAndProject({ url: url }) + handleClose() + } return ( @@ -32,7 +32,7 @@ const LoadUrlPopup: FC<{ - ); -}; + ) +} -export default LoadUrlPopup; +export default LoadUrlPopup diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx index 471c5c3e..40ea15fd 100644 --- a/client/src/Popups/LoadZulip.tsx +++ b/client/src/Popups/LoadZulip.tsx @@ -1,42 +1,47 @@ -import { Popup } from '../Navigation'; -import { FC, FormEvent, useRef, useState } from 'react'; +import { FormEvent, useRef, useState } from 'react' -const LoadZulipPopup: FC<{ - open: boolean; - handleClose: () => void; - setContent: (code: string) => void; -}> = ({ open, handleClose, setContent }) => { - const [error, setError] = useState(''); - const textInputRef = useRef(null); +import { Popup } from '../navigation/Popup' + +function LoadZulipPopup({ + open, + handleClose, + setContent, +}: { + open: boolean + handleClose: () => void + setContent: (code: string) => void +}) { + const [error, setError] = useState('') + const textInputRef = useRef(null) const handleLoad = (ev: FormEvent) => { - ev.preventDefault(); - let md = textInputRef.current?.value; // TODO: not a URL but text, update the var names + ev.preventDefault() + let md = textInputRef.current?.value // TODO: not a URL but text, update the var names - console.log(`received: ${md}`); + console.log(`received: ${md}`) // regex 1 finds the code-blocks - let regex1 = /(`{3,})\s*(lean)?\s*\n(.+?)\1/gs; + let regex1 = /(`{3,})\s*(lean)?\s*\n(.+?)\1/gs // regex 2 extracts the code from a codeblock - let regex2 = /^(`{3,})\s*(?:lean)?\s*\n\s*(.+)\s*\1$/s; + let regex2 = /^(`{3,})\s*(?:lean)?\s*\n\s*(.+)\s*\1$/s - let res = md?.match(regex1); + let res = md?.match(regex1) if (res) { let code = res .map((s) => { - return s.match(regex2)![2]; + return s.match(regex2)![2] }) .join('\n\n-- new codeblock\n\n') - .trim() + '\n'; - setContent(code); + .trim() + '\n' + setContent(code) //setError('') - handleClose(); + handleClose() } else { - setError('Could not find a code-block in the message'); + setError('Could not find a code-block in the message') } - }; + } return ( @@ -56,7 +61,7 @@ const LoadZulipPopup: FC<{ - ); -}; + ) +} -export default LoadZulipPopup; +export default LoadZulipPopup diff --git a/client/src/Popups/PrivacyPolicy.tsx b/client/src/Popups/PrivacyPolicy.tsx index 95573766..bf06b4f0 100644 --- a/client/src/Popups/PrivacyPolicy.tsx +++ b/client/src/Popups/PrivacyPolicy.tsx @@ -1,12 +1,8 @@ -import { FC } from 'react'; -import { Popup } from '../Navigation'; -import lean4webConfig from '../config/config'; +import lean4webConfig from '../config/config' +import { Popup } from '../navigation/Popup' /** The popup with the privacy policy. */ -const PrivacyPopup: FC<{ - open: boolean; - handleClose: () => void; -}> = ({ open, handleClose }) => { +function PrivacyPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) { return (

Privacy Policy

@@ -34,7 +30,7 @@ const PrivacyPopup: FC<{

)} - ); -}; + ) +} -export default PrivacyPopup; +export default PrivacyPopup diff --git a/client/src/Popups/Tools.tsx b/client/src/Popups/Tools.tsx index ff5b4cf3..8e00db34 100644 --- a/client/src/Popups/Tools.tsx +++ b/client/src/Popups/Tools.tsx @@ -1,36 +1,37 @@ -import { Popup } from '../Navigation'; -import { FC, useEffect, useRef, useState } from 'react'; +import { useEffect, useRef, useState } from 'react' + +import { Popup } from '../navigation/Popup' // TODO: Do these interfaces exist somewhere in vscode-lean4? // They might need to be updated manually if changes to `lake` occur. interface LakePackage { - url: string; - type: 'git'; - subDir: string; - scope: string; - rev: string; - name: string; - manifestFile: string; - inputRev: string; - inherited: string; - configFile: string; + url: string + type: 'git' + subDir: string + scope: string + rev: string + name: string + manifestFile: string + inputRev: string + inherited: string + configFile: string } interface LocalLakePackage { - type: 'path'; - name: string; - manifestFile: string; - inherited: false; - dir: string; - configFile: string; + type: 'path' + name: string + manifestFile: string + inherited: false + dir: string + configFile: string } interface LakeManifest { - version: string; - packagesDir: string; - packages: (LakePackage | LocalLakePackage)[]; - name: string; - lakeDir: string; + version: string + packagesDir: string + packages: (LakePackage | LocalLakePackage)[] + name: string + lakeDir: string } /** Default. Should never actually be visible to the user as it will be overwritten immediately */ @@ -40,26 +41,26 @@ const emptyManifest: LakeManifest = { packages: [], name: '', lakeDir: '', -}; +} /** These are just a few relevant fields the data fetched from github comprises. */ interface CommitInfo { - sha: string; + sha: string commit: { author: { - name: string; - date: string; - }; - message: string; - }; + name: string + date: string + } + message: string + } author: { - avatar_url: string; - }; + avatar_url: string + } stats: { - total: number; - additions: number; - deletions: number; - }; + total: number + additions: number + deletions: number + } } /** Displays a link of the specified commit together with a hover-tooltip showing the @@ -68,62 +69,60 @@ interface CommitInfo { * Note that github has a rate limit (60 requests/h), but since this should be a * rarely used feature, it might be fine for now. */ -const ToolTip: FC<{ - pkg: LakePackage; -}> = ({ pkg }) => { - const [loaded, setLoaded] = useState(false); - const linkRef = useRef(null); - const [commit, setCommit] = useState(); - const [error, setError] = useState(); - - useEffect(() => { - linkRef.current?.addEventListener('mouseover', handleHover); - return () => { - linkRef.current?.removeEventListener('mouseover', handleHover); - }; - }, [linkRef, loaded]); +function ToolTip({ pkg }: { pkg: LakePackage }) { + const [loaded, setLoaded] = useState(false) + const linkRef = useRef(null) + const [commit, setCommit] = useState() + const [error, setError] = useState() // Load commit info on hovering the first time const handleHover = (_event: any) => { // Do not fetch twice if (loaded) { - return; + return } - setLoaded(true); + setLoaded(true) // construct github api URL from repo URL - let m = pkg.url.match(/github.com\/([^\/]+)\/([^\/\.]+)/i); // exclude '\.' to strip potential '.git' at the end + let m = pkg.url.match(/github.com\/([^\/]+)\/([^\/\.]+)/i) // exclude '\.' to strip potential '.git' at the end if (!m || m.length < 2) { - console.warn(`[LeanWeb]: cannot parse package url`, pkg.url); - setError('Not Found'); - return; + console.warn(`[LeanWeb]: cannot parse package url`, pkg.url) + setError('Not Found') + return } - let githubUrl = `https://api.github.com/repos/${m![1]}/${m![2]}/commits/${pkg.rev}`; + let githubUrl = `https://api.github.com/repos/${m![1]}/${m![2]}/commits/${pkg.rev}` - pkg.url.replace('github.com/', 'api.github.com/repos/') + `/commits/${pkg.rev}`; - console.debug(`[LeanWeb]: fetch from ${githubUrl}`); + pkg.url.replace('github.com/', 'api.github.com/repos/') + `/commits/${pkg.rev}` + console.debug(`[LeanWeb]: fetch from ${githubUrl}`) fetch(githubUrl) .then((response) => { if (!response.ok) { - console.warn(`[LeanWeb]: failed request (${response.status})`, response); + console.warn(`[LeanWeb]: failed request (${response.status})`, response) } - return response.json(); + return response.json() }) .then((data) => { if (data.message) { // e.g. when reaching rate limit - setError(data.message); + setError(data.message) } else { - setCommit(data); + setCommit(data) } }) .catch((error) => { - setError(error); - console.error(error); - }); - }; + setError(error) + console.error(error) + }) + } + + useEffect(() => { + linkRef.current?.addEventListener('mouseover', handleHover) + return () => { + linkRef.current?.removeEventListener('mouseover', handleHover) + } + }, [linkRef, loaded]) return ( @@ -151,53 +150,57 @@ const ToolTip: FC<{ )}
- ); -}; + ) +} /** Shows important information about the Lean project loaded in the web editor */ -const ToolsPopup: FC<{ - open: boolean; - project: string; - handleClose: () => void; -}> = ({ open, handleClose, project }) => { - const [manifest, setManifest] = useState(emptyManifest); - const [toolchain, setToolchain] = useState(''); +function ToolsPopup({ + open, + handleClose, + project, +}: { + open: boolean + project: string + handleClose: () => void +}) { + const [manifest, setManifest] = useState(emptyManifest) + const [toolchain, setToolchain] = useState('') // The last time `lake-manifest.json` has been modified // Experimental: This might somewhat agree with the last update of the project // I couldn't think of a better way to determine this. - const [lastModified, setLastModified] = useState(null); + const [lastModified, setLastModified] = useState(null) // Load the new manifest & toolchain useEffect(() => { if (!project) { - return; + return } - const urlManifest = `${window.location.origin}/api/manifest/${project}`; + const urlManifest = `${window.location.origin}/api/manifest/${project}` fetch(urlManifest) .then((response) => { - var _lastModified = response.headers.get('Last-Modified'); + var _lastModified = response.headers.get('Last-Modified') response.json().then((manifest) => { - setManifest(manifest); - setLastModified(_lastModified); - }); + setManifest(manifest) + setLastModified(_lastModified) + }) }) .catch((err) => { - console.error('Error reading manifest.'); - console.error(err); - }); + console.error('Error reading manifest.') + console.error(err) + }) - const urlToolchain = `${window.location.origin}/api/toolchain/${project}`; + const urlToolchain = `${window.location.origin}/api/toolchain/${project}` fetch(urlToolchain) .then((response) => { response.text().then((toolchain) => { - setToolchain(toolchain); - }); + setToolchain(toolchain) + }) }) .catch((err) => { - console.error('Error reading toolchain.'); - console.error(err); - }); - }, [project]); + console.error('Error reading toolchain.') + console.error(err) + }) + }, [project]) return ( @@ -259,7 +262,7 @@ const ToolsPopup: FC<{ #eval Lean.versionString - ); -}; + ) +} -export default ToolsPopup; +export default ToolsPopup diff --git a/client/src/config/config.tsx b/client/src/config/config.tsx index 93b85edd..93125e58 100644 --- a/client/src/config/config.tsx +++ b/client/src/config/config.tsx @@ -1,4 +1,4 @@ -import { LeanWebConfig } from './docs'; // look here for documentation of the individual config options +import { LeanWebConfig } from './docs' // look here for documentation of the individual config options const lean4webConfig: LeanWebConfig = { projects: [ @@ -17,6 +17,6 @@ const lean4webConfig: LeanWebConfig = { serverCountry: null, contactDetails: null, impressum: null, -}; +} -export default lean4webConfig; +export default lean4webConfig diff --git a/client/src/config/docs.tsx b/client/src/config/docs.tsx index c70f14a9..2632a6d8 100644 --- a/client/src/config/docs.tsx +++ b/client/src/config/docs.tsx @@ -2,16 +2,16 @@ * This file contains the documentation of the existing `config` options */ -import { JSX } from 'react'; +import { JSX } from 'react' /** An example can be any Lean file which belongs to the project. * The editor just reads the file content, but it makes sense for maintainability * that you ensure the Lean project actually builds the file. */ interface LeanWebExample { /** File to load; relative path in `lean4web/Projects//` */ - file: string; + file: string /** Display name used in the `Examples` menu */ - name: string; + name: string } /** You can add any Lean Project under `lean4web/Projects/` and add it here to use it in the @@ -23,27 +23,27 @@ interface LeanWebProject { /** The folder containing the Lean project; the folder is expected to be in `lean4web/Projects/`. * The folder name will appear in the URL. */ - folder: string; + folder: string /** Display name; shown in selection menu */ - name: string; + name: string /** A list of examples which are added under the menu `Examples` */ - examples?: LeanWebExample[]; + examples?: LeanWebExample[] } interface LeanWebConfig { - projects: LeanWebProject[]; + projects: LeanWebProject[] /** Where the server is located. Use `null` to not display this information. */ - serverCountry: string | null; + serverCountry: string | null /** Contact details of the server maintainer. Used in Privacy Policy and Impressum. * Use `null` to not display this information. * Note: This will be embedded inside a `

` tag! (example: `<>Hans Muster
hans@nowhere.com`) */ - contactDetails: JSX.Element | null; + contactDetails: JSX.Element | null /** Additional legal information shown in impressum alongside the contact details. * Use `null` to not display this information. * (example: `<>

vat number: 000

<>`) */ - impressum: JSX.Element | null; + impressum: JSX.Element | null } -export type { LeanWebExample, LeanWebProject, LeanWebConfig }; +export type { LeanWebConfig, LeanWebExample, LeanWebProject } diff --git a/client/src/editor/code-atoms.ts b/client/src/editor/code-atoms.ts new file mode 100644 index 00000000..16af6f54 --- /dev/null +++ b/client/src/editor/code-atoms.ts @@ -0,0 +1,53 @@ +import { atom } from 'jotai' +import LZString from 'lz-string' + +import { settingsAtom } from '../settings/settings-atoms' +import { freshlyImportedCodeAtom, importedCodeAtom, importUrlAtom } from '../store/import-atoms' +import { urlArgsAtom, urlArgsStableAtom } from '../store/url-atoms' +import { fixedEncodeURIComponent } from '../utils/UrlParsing' + +/** Atom which represents the editor content and synchronises it with the url hash. */ +export const codeAtom = atom( + (get) => { + const urlArgs = get(urlArgsStableAtom) + if (urlArgs.code) { + return decodeURIComponent(urlArgs.code) + } + if (urlArgs.codez) { + return LZString.decompressFromBase64(urlArgs.codez) + } + return get(freshlyImportedCodeAtom) + }, + (get, set, code: string) => { + const urlArgs = get(urlArgsAtom) + if (code.length == 0) { + // delete all url arguments if there is no code + set(urlArgsAtom, { ...urlArgs, url: undefined, code: undefined, codez: undefined }) + return + } + if (urlArgs.url) { + // store freshly imported code and the URL so we can compare later + const freshlyImportedCode = get(freshlyImportedCodeAtom) + set(importedCodeAtom, freshlyImportedCode) + set(importUrlAtom, urlArgs.url) + } else { + // if the code matches previously imported code, display the URL instead + const importedCode = get(importedCodeAtom) + if (importedCode !== undefined && importedCode === code) { + const importUrl = get(importUrlAtom) + set(urlArgsAtom, { ...urlArgs, url: importUrl, code: undefined, codez: undefined }) + return + } + } + const compress = get(settingsAtom).compress + if (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 compressedCode = LZString.compressToBase64(code).replace(/=*$/, '') + set(urlArgsAtom, { ...urlArgs, url: undefined, code: undefined, codez: compressedCode }) + } else { + const encodedCode = fixedEncodeURIComponent(code) + set(urlArgsAtom, { ...urlArgs, url: undefined, code: encodedCode, codez: undefined }) + } + }, +) diff --git a/client/src/index.tsx b/client/src/index.tsx index c2818776..25e51d79 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -1,10 +1,12 @@ -import ReactDOM from 'react-dom/client'; -import App from './App.tsx'; -import './css/index.css'; -import { StrictMode } from 'react'; +import './css/index.css' + +import { StrictMode } from 'react' +import ReactDOM from 'react-dom/client' + +import App from './App.tsx' ReactDOM.createRoot(document.getElementById('root')!).render( , -); +) diff --git a/client/src/navigation/Dropdown.tsx b/client/src/navigation/Dropdown.tsx new file mode 100644 index 00000000..f3f922da --- /dev/null +++ b/client/src/navigation/Dropdown.tsx @@ -0,0 +1,53 @@ +import { IconDefinition } from '@fortawesome/free-solid-svg-icons' +import { MouseEventHandler, ReactNode } from 'react' + +import { NavButton } from './NavButton' + +/** A button to appear in the hamburger menu or to navigation bar. */ +export function Dropdown({ + open, + setOpen, + icon, + text, + useOverlay = false, + onClick, + children, +}: { + open: boolean + setOpen: (open: boolean) => void + icon?: IconDefinition + text?: string + useOverlay?: boolean + onClick?: MouseEventHandler + children?: ReactNode +}) { + return ( + <> +
+ { + setOpen(!open) + onClick!(ev) + ev.stopPropagation() + }} + /> + {open && ( +
setOpen(false)}> + {children} +
+ )} +
+ {useOverlay && open && ( +
{ + setOpen(false) + ev.stopPropagation() + }} + /> + )} + + ) +} diff --git a/client/src/navigation/NavButton.tsx b/client/src/navigation/NavButton.tsx new file mode 100644 index 00000000..ad403b03 --- /dev/null +++ b/client/src/navigation/NavButton.tsx @@ -0,0 +1,26 @@ +import { IconDefinition } from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { JSX, MouseEventHandler } from 'react' + +/** A button to appear in the hamburger menu or to navigation bar. */ +export function NavButton({ + icon, + iconElement, + text, + onClick = () => {}, + href = undefined, +}: { + icon?: IconDefinition + iconElement?: JSX.Element + text: string + onClick?: MouseEventHandler + href?: string +}) { + // note: it seems that we can just leave the `target="_blank"` and it has no + // effect on links without a `href`. If not, add `if (href)` statement here... + return ( + + {iconElement ?? } {text} + + ) +} diff --git a/client/src/navigation/Navigation.tsx b/client/src/navigation/Navigation.tsx new file mode 100644 index 00000000..7bed6250 --- /dev/null +++ b/client/src/navigation/Navigation.tsx @@ -0,0 +1,302 @@ +import '../css/Modal.css' +import '../css/Navigation.css' + +import { faArrowRotateRight, faCode, faInfoCircle } from '@fortawesome/free-solid-svg-icons' +import { + faArrowUpRightFromSquare, + faBars, + faCloudArrowUp, + faDownload, + faGear, + faHammer, + faShield, + faStar, + faUpload, + faXmark, +} from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { useAtom } from 'jotai' +import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react' + +import ZulipIcon from '../assets/zulip.svg' +import lean4webConfig from '../config/config' +import { codeAtom } from '../editor/code-atoms' +import ImpressumPopup from '../Popups/Impressum' +import LoadUrlPopup from '../Popups/LoadUrl' +import LoadZulipPopup from '../Popups/LoadZulip' +import PrivacyPopup from '../Popups/PrivacyPolicy' +import ToolsPopup from '../Popups/Tools' +import { mobileAtom } from '../settings/settings-atoms' +import { SettingsPopup } from '../settings/SettingsPopup' +import { setImportUrlAndProjectAtom } from '../store/import-atoms' +import { projectAtom } from '../store/project-atoms' +import { save } from '../utils/SaveToFile' +import { Dropdown } from './Dropdown' +import { NavButton } from './NavButton' + +/** The menu items either appearing inside the dropdown or outside */ +function FlexibleMenu({ + isInDropdown = false, + setOpenNav, + openExample, + setOpenExample, + openLoad, + setOpenLoad, + setContent, + setLoadUrlOpen, + setLoadZulipOpen, +}: { + isInDropdown: boolean + setOpenNav: Dispatch> + openExample: boolean + setOpenExample: Dispatch> + openLoad: boolean + setOpenLoad: Dispatch> + setContent: (code: string) => void + setLoadUrlOpen: Dispatch> + setLoadZulipOpen: Dispatch> +}) { + const [, setImportUrlAndProject] = useAtom(setImportUrlAndProjectAtom) + const loadFileFromDisk = (event: ChangeEvent) => { + console.debug('Loading file from disk') + const fileToLoad = event.target.files![0] + var fileReader = new FileReader() + fileReader.onload = (fileLoadedEvent) => { + var textFromFileLoaded = fileLoadedEvent.target!.result as string + setContent(textFromFileLoaded) + } + fileReader.readAsText(fileToLoad, 'UTF-8') + // Manually close the menu as we prevent it closing below. + setOpenLoad(false) + } + + return ( + <> + { + setOpenLoad(false) + !isInDropdown && setOpenNav(false) + }} + > + {lean4webConfig.projects.map((proj) => + proj.examples?.map((example) => ( + { + setImportUrlAndProject({ + url: `${window.location.origin}/api/example/${proj.folder}/${example.file}`, + project: proj.folder, + }) + setOpenExample(false) + }} + /> + )), + )} + + { + setOpenExample(false) + !isInDropdown && setOpenNav(false) + }} + > + ev.stopPropagation()} + /> + {/* Need `ev.stopPropagation` to prevent closing until the file is loaded. + Otherwise the file-upload is destroyed too early. */} + + { + setLoadUrlOpen(true) + }} + /> + } + text="Load Zulip Message" + onClick={() => { + setLoadZulipOpen(true) + }} + /> + + + ) +} + +/** The Navigation menu */ +export function Menu({ + setContent, + restart, + codeMirror, + setCodeMirror, +}: { + setContent: (code: string) => void + restart?: () => void + codeMirror: boolean + setCodeMirror: Dispatch> +}) { + const [project, setProject] = useAtom(projectAtom) + const [code] = useAtom(codeAtom) + + // state for handling the dropdown menus + const [openNav, setOpenNav] = useState(false) + const [openExample, setOpenExample] = useState(false) + const [openLoad, setOpenLoad] = useState(false) + const [loadUrlOpen, setLoadUrlOpen] = useState(false) + const [loadZulipOpen, setLoadZulipOpen] = useState(false) + + // state for the popups + const [privacyOpen, setPrivacyOpen] = useState(false) + const [impressumOpen, setImpressumOpen] = useState(false) + const [toolsOpen, setToolsOpen] = useState(false) + const [settingsOpen, setSettingsOpen] = useState(false) + + const [mobile] = useAtom(mobileAtom) + + const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails + + return ( +
+ + {mobile && ( + { + setCodeMirror(!codeMirror) + }} + /> + )} + {!mobile && ( + + )} + { + setOpenExample(false) + setOpenLoad(false) + }} + > + {mobile && ( + + )} + { + setSettingsOpen(true) + }} + /> + setToolsOpen(true)} /> + + { + if (code !== undefined) save(code) + }} + /> + { + setPrivacyOpen(true) + }} + /> + {hasImpressum && ( + { + setImpressumOpen(true) + }} + /> + )} + + + + + setPrivacyOpen(false)} /> + {hasImpressum && ( + setImpressumOpen(false)} /> + )} + setToolsOpen(false)} project={project} /> + setSettingsOpen(false)} + closeNav={() => setOpenNav(false)} + /> + setLoadUrlOpen(false)} /> + setLoadZulipOpen(false)} + setContent={setContent} + /> +
+ ) +} diff --git a/client/src/navigation/Popup.tsx b/client/src/navigation/Popup.tsx new file mode 100644 index 00000000..9c558d0b --- /dev/null +++ b/client/src/navigation/Popup.tsx @@ -0,0 +1,22 @@ +import { ReactNode } from 'react' + +/** A popup which overlays the entire screen. */ +export function Popup({ + open, + handleClose, + children, +}: { + open: boolean + handleClose: () => void // TODO: what's the correct type? + children?: ReactNode +}) { + return ( +
+
+
+
+ {children} +
+
+ ) +} diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index a34eac48..c367b6e5 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -1,43 +1,39 @@ -import Box from '@mui/material/Box'; -import Slider from '@mui/material/Slider'; -import Switch from '@mui/material/Switch'; -import { useAtom } from 'jotai/react'; -import { useState } from 'react'; -import { Popup } from '../Navigation'; -import { applySettingsAtom, settingsAtom } from './settings-atoms'; -import { defaultSettings, Settings } from './settings-types'; -import type { MobileValues, Theme } from './settings-types'; -import { shallowEqualSubset } from '../utils/shallowEqual'; -import { inputAdornmentClasses } from '@mui/material/InputAdornment'; +import Box from '@mui/material/Box' +import Slider from '@mui/material/Slider' +import Switch from '@mui/material/Switch' +import { useAtom } from 'jotai/react' +import { useState } from 'react' + +import { Popup } from '../navigation/Popup' +import { shallowEqualSubset } from '../utils/shallowEqual' +import { applySettingsAtom, settingsAtom } from './settings-atoms' +import type { MobileValues, Theme } from './settings-types' +import { defaultSettings, Settings } from './settings-types' export function SettingsPopup({ open, handleClose, closeNav, - project, - setProject, }: { - open: boolean; - handleClose: () => void; - closeNav: () => void; - project: string; - setProject: (project: string) => void; + open: boolean + handleClose: () => void + closeNav: () => void }) { - const [settings, setSettings] = useAtom(settingsAtom); - const [, applySettings] = useAtom(applySettingsAtom); - const [newSettings, setNewSettings] = useState(settings); + const [settings, setSettings] = useAtom(settingsAtom) + const [, applySettings] = useAtom(applySettingsAtom) + const [newSettings, setNewSettings] = useState(settings) function updateSetting(key: K, value: Settings[K]) { - setNewSettings((prev) => ({ ...prev, [key]: value })); + setNewSettings((prev) => ({ ...prev, [key]: value })) } return (
{ - ev.preventDefault(); - handleClose(); - closeNav(); + ev.preventDefault() + handleClose() + closeNav() }} > {/*

Project settings

@@ -67,7 +63,7 @@ export function SettingsPopup({ id="abbreviationCharacter" type="text" onChange={(ev) => { - updateSetting('abbreviationCharacter', ev.target.value); + updateSetting('abbreviationCharacter', ev.target.value) }} value={newSettings.abbreviationCharacter} /> @@ -76,7 +72,7 @@ export function SettingsPopup({ { - updateSetting('wordWrap', !newSettings.wordWrap); + updateSetting('wordWrap', !newSettings.wordWrap) }} checked={newSettings.wordWrap} /> @@ -86,7 +82,7 @@ export function SettingsPopup({ { - updateSetting('acceptSuggestionOnEnter', !newSettings.acceptSuggestionOnEnter); + updateSetting('acceptSuggestionOnEnter', !newSettings.acceptSuggestionOnEnter) }} checked={newSettings.acceptSuggestionOnEnter} /> @@ -96,7 +92,7 @@ export function SettingsPopup({ { - updateSetting('showGoalNames', !newSettings.showGoalNames); + updateSetting('showGoalNames', !newSettings.showGoalNames) }} checked={newSettings.showGoalNames} /> @@ -106,7 +102,7 @@ export function SettingsPopup({ { - updateSetting('showExpectedType', !newSettings.showExpectedType); + updateSetting('showExpectedType', !newSettings.showExpectedType) }} checked={newSettings.showExpectedType} /> @@ -121,7 +117,7 @@ export function SettingsPopup({ name="theme" value={newSettings.theme} onChange={(ev) => { - updateSetting('theme', ev.target.value as Theme); + updateSetting('theme', ev.target.value as Theme) }} > @@ -145,7 +141,7 @@ export function SettingsPopup({ '& .MuiSlider-track': { display: 'none' }, }} onChange={(_, val) => { - updateSetting('mobile', mobileSliderMarks[val].key); + updateSetting('mobile', mobileSliderMarks[val].key) }} /> @@ -154,7 +150,7 @@ export function SettingsPopup({ { - updateSetting('compress', !newSettings.compress); + updateSetting('compress', !newSettings.compress) }} checked={newSettings.compress} /> @@ -164,7 +160,7 @@ export function SettingsPopup({ { - updateSetting('inUrl', !newSettings.inUrl); + updateSetting('inUrl', !newSettings.inUrl) }} checked={newSettings.inUrl} /> @@ -178,7 +174,7 @@ export function SettingsPopup({ { - updateSetting('saved', !newSettings.saved); + updateSetting('saved', !newSettings.saved) }} checked={newSettings.saved} /> @@ -189,8 +185,8 @@ export function SettingsPopup({