From 7f17d773fb43c4a1355ada78b40fd1e1596b9e12 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 16:33:26 +0100 Subject: [PATCH] prettier & tailwind --- .editorconfig | 9 + .eslintrc.cjs | 18 +- .vscode/settings.json | 4 + Projects/MathlibDemo/lake-manifest.json | 211 +++--- Projects/README.md | 4 +- Projects/Stable/lake-manifest.json | 12 +- README.md | 13 +- client/src/.prettierrc.json | 14 + client/src/App.tsx | 538 +++++++------- client/src/Navigation.tsx | 540 +++++++++----- client/src/Popups/Impressum.tsx | 39 +- client/src/Popups/LoadUrl.tsx | 51 +- client/src/Popups/LoadZulip.tsx | 83 ++- client/src/Popups/PrivacyPolicy.tsx | 58 +- client/src/Popups/Tools.tsx | 382 +++++----- client/src/config/config.tsx | 40 +- client/src/config/docs.tsx | 25 +- client/src/css/App.css | 2 +- client/src/css/Editor.css | 53 +- client/src/css/Modal.css | 18 +- client/src/css/Navigation.css | 22 +- client/src/css/index.css | 8 +- client/src/index.tsx | 10 +- client/src/settings/SettingsPopup.tsx | 290 +++++--- client/src/settings/settings-atoms.ts | 72 +- client/src/settings/settings-types.ts | 40 +- .../src/settings/settings-url-converters.ts | 82 ++- client/src/store/location-atoms.ts | 4 +- client/src/store/window-atoms.ts | 4 +- client/src/utils/Entries.ts | 2 +- client/src/utils/SaveToFile.tsx | 6 +- client/src/utils/UrlParsing.tsx | 48 +- client/src/utils/WindowWidth.tsx | 19 +- client/src/utils/cleanObject.ts | 4 +- client/src/utils/shallowEqual.ts | 6 +- client/src/vite-env.d.ts | 10 +- cypress.config.ts | 28 +- cypress/e2e/settings.cy.ts | 96 +-- cypress/e2e/spec.cy.ts | 383 +++++----- cypress/support/assertions.ts | 20 +- cypress/support/commands.ts | 42 +- cypress/support/e2e.ts | 18 +- cypress/support/index.d.ts | 72 +- cypress/tsconfig.json | 14 +- doc/Development.md | 3 +- doc/Installation.md | 5 +- doc/Troubleshoot.md | 2 +- doc/Usage.md | 4 +- ecosystem.config.cjs | 18 +- index.html | 10 +- package-lock.json | 664 ++++++++++++++++-- package.json | 3 + server/index.mjs | 280 ++++---- vite.config.ts | 82 ++- 54 files changed, 2779 insertions(+), 1706 deletions(-) create mode 100644 .editorconfig create mode 100644 .vscode/settings.json create mode 100644 client/src/.prettierrc.json diff --git a/.editorconfig b/.editorconfig new file mode 100644 index 00000000..9d08a1a8 --- /dev/null +++ b/.editorconfig @@ -0,0 +1,9 @@ +root = true + +[*] +charset = utf-8 +indent_style = space +indent_size = 2 +end_of_line = lf +insert_final_newline = true +trim_trailing_whitespace = true diff --git a/.eslintrc.cjs b/.eslintrc.cjs index d6c95379..6e8698b7 100644 --- a/.eslintrc.cjs +++ b/.eslintrc.cjs @@ -2,17 +2,17 @@ module.exports = { root: true, env: { browser: true, es2020: true }, extends: [ - 'eslint:recommended', - 'plugin:@typescript-eslint/recommended', - 'plugin:react-hooks/recommended', + "eslint:recommended", + "plugin:@typescript-eslint/recommended", + "plugin:react-hooks/recommended", ], - ignorePatterns: ['dist', '.eslintrc.cjs'], - parser: '@typescript-eslint/parser', - plugins: ['react-refresh'], + ignorePatterns: ["dist", ".eslintrc.cjs"], + parser: "@typescript-eslint/parser", + plugins: ["react-refresh"], rules: { - 'react-refresh/only-export-components': [ - 'warn', + "react-refresh/only-export-components": [ + "warn", { allowConstantExport: true }, ], }, -} +}; diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 00000000..d1b4edb2 --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,4 @@ +{ + "editor.formatOnSave": true, + "editor.defaultFormatter": "esbenp.prettier-vscode" +} \ No newline at end of file diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json index e260cef0..5c3d298e 100644 --- a/Projects/MathlibDemo/lake-manifest.json +++ b/Projects/MathlibDemo/lake-manifest.json @@ -1,95 +1,116 @@ -{"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": "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" +} diff --git a/Projects/README.md b/Projects/README.md index 7d205994..deb77a22 100644 --- a/Projects/README.md +++ b/Projects/README.md @@ -39,11 +39,9 @@ the file from `Projects/MyCoolProject/MyCoolProject/Demo1.lean`. You might want to look at the provided `MathlibDemo` project for comparison. - **Important**: In order for lake to use any "leanOptions" specified in the projects lakefile, you must make sure there is a file `Projects/MyCoolProject/MyCoolProject.lean` where folder name and file name coincide. - ## Creating Lean Projects with Mathlib To create a Lean project with a specific version and mathlib dependencies, you can use the `create_project.sh` script: @@ -53,6 +51,7 @@ To create a Lean project with a specific version and mathlib dependencies, you c ``` The version should be in the format of `v4.x.x` or `4.x.x`. For example: + ```bash ./create_project.sh v4.13.0 # or @@ -60,6 +59,7 @@ The version should be in the format of `v4.x.x` or `4.x.x`. For example: ``` This will: + 1. Create a new Lean project in `Projects//` 2. Configure mathlib dependencies 3. Build the project with cache diff --git a/Projects/Stable/lake-manifest.json b/Projects/Stable/lake-manifest.json index 19497751..1d38c03d 100644 --- a/Projects/Stable/lake-manifest.json +++ b/Projects/Stable/lake-manifest.json @@ -1,5 +1,7 @@ -{"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/README.md b/README.md index ab1ac5a1..85d8bd26 100644 --- a/README.md +++ b/README.md @@ -1,7 +1,6 @@ [![GitHub license](https://img.shields.io/badge/License-Apache_2.0-blue.svg)](https://github.com/leanprover-community/lean4web/blob/main/LICENSE) [![(Runtime) Build and Test](https://github.com/leanprover-community/lean4web/actions/workflows/build.yml/badge.svg)](https://github.com/leanprover-community/lean4web/actions/workflows/build.yml) - # Lean 4 Web This is a web version of Lean 4. There is a playground hosted at [live.lean-lang.org](https://live.lean-lang.org) and one at [lean.math.hhu.de](https://lean.math.hhu.de). @@ -11,11 +10,11 @@ running on a web server, and not in the browser. ## Scope of lean4web -* Provide a clean, minimalistic and easily accessible way to run some (smallish) Lean snippets -* Provide a simple way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed. -* Provide a easy way to demonstrate some Lean code in talks/lecutres. -* Provide a easy way for newcomers to doodle with Lean before installing it. -* Provide a way to run some Lean code in a mobile context. +- Provide a clean, minimalistic and easily accessible way to run some (smallish) Lean snippets +- Provide a simple way to run [MWEs](https://leanprover-community.github.io/mwe.html) from [Zulip](https://leanprover.zulipchat.com) with the latest [Mathlib](https://github.com/leanprover-community/mathlib4) installed. +- Provide a easy way to demonstrate some Lean code in talks/lecutres. +- Provide a easy way for newcomers to doodle with Lean before installing it. +- Provide a way to run some Lean code in a mobile context. Currently, serious Lean code development and larger projects are considered out-of-scope. For these, it might be more suitable to look at a setup using Codespaces or Gitpot. @@ -27,7 +26,7 @@ If you experience any problems, or have feature requests, please open an issue h PRs fixing issues are very welcome! -For new features, it's best to write an issue first to discuss them: For example, some functionality might be better implemented in [lean4monaco](https://github.com/hhu-adam/lean4monaco) which provides the key features and a discussion might be helpful to figure this out. +For new features, it's best to write an issue first to discuss them: For example, some functionality might be better implemented in [lean4monaco](https://github.com/hhu-adam/lean4monaco) which provides the key features and a discussion might be helpful to figure this out. ## Documentation diff --git a/client/src/.prettierrc.json b/client/src/.prettierrc.json new file mode 100644 index 00000000..70ae7996 --- /dev/null +++ b/client/src/.prettierrc.json @@ -0,0 +1,14 @@ +{ + "printWidth": 100, + "tabWidth": 2, + "useTabs": false, + "semi": true, + "singleQuote": true, + "quoteProps": "as-needed", + "jsxSingleQuote": false, + "trailingComma": "all", + "bracketSpacing": true, + "bracketSameLine": false, + "arrowParens": "always", + "endOfLine": "lf" +} diff --git a/client/src/App.tsx b/client/src/App.tsx index b12da7c7..01bcd32f 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,104 +1,109 @@ -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 { 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'; /** 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 [searchParams] = useAtom(settingsUrlAtom); // Lean4monaco options const [options, setOptions] = useState({ // placeholder, updated below - websocket: { url: '' } - }) + 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) + 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 [code, setCode] = useState(''); + const [project, setProject] = useState('MathlibDemo'); + const [url, setUrl] = useState(null); + const [codeFromUrl, setCodeFromUrl] = useState(''); /** 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() + console.log('[Lean4web] Parsing URL'); + let args = parseArgs(); if (args.code) { - let _code = decodeURIComponent(args.code) - setContent(_code) + 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(lookupUrl(decodeURIComponent(args.url)))} + if (args.url) { + setUrl(lookupUrl(decodeURIComponent(args.url))); + } // if no project provided, use default - let project = args.project ?? 'MathlibDemo' + let project = args.project ?? 'MathlibDemo'; - console.log(`[Lean4web] Setting project to ${project}`) - setProject(project) - }, []) + 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') - - var socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + - window.location.host + "/websocket/" + project - console.log(`[Lean4web] Socket url is ${socketUrl}`) + 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}`); var _options: LeanMonacoOptions = { - websocket: {url: socketUrl}, + websocket: { url: socketUrl }, // Restrict monaco's extend (e.g. context menu) to the editor itself htmlElement: editorRef.current ?? undefined, vscode: { @@ -106,118 +111,127 @@ function App() { * for the desired setting, select "Copy Setting as JSON" from the "More Actions" * menu next to the selected setting, and paste the copied string here. */ - "workbench.colorTheme": settings.theme, - "editor.tabSize": 2, + 'workbench.colorTheme': settings.theme, + 'editor.tabSize': 2, // "editor.rulers": [100], - "editor.lightbulb.enabled": "on", - "editor.wordWrap": settings.wordWrap ? "on" : "off", - "editor.wrappingStrategy": "advanced", - "editor.semanticHighlighting.enabled": true, - "editor.acceptSuggestionOnEnter": settings.acceptSuggestionOnEnter ? "on" : "off", - "lean4.input.eagerReplacementEnabled": true, - "lean4.infoview.showGoalNames": settings.showGoalNames, - "lean4.infoview.emphasizeFirstGoal": true, - "lean4.infoview.showExpectedType": settings.showExpectedType, - "lean4.infoview.showTooltipOnHover": false, - "lean4.input.leader": settings.abbreviationCharacter - } - } - setOptions(_options) - }, [editorRef, project, settings]) + 'editor.lightbulb.enabled': 'on', + 'editor.wordWrap': settings.wordWrap ? 'on' : 'off', + 'editor.wrappingStrategy': 'advanced', + 'editor.semanticHighlighting.enabled': true, + 'editor.acceptSuggestionOnEnter': settings.acceptSuggestionOnEnter ? 'on' : 'off', + 'lean4.input.eagerReplacementEnabled': true, + 'lean4.infoview.showGoalNames': settings.showGoalNames, + 'lean4.infoview.emphasizeFirstGoal': true, + 'lean4.infoview.showExpectedType': settings.showExpectedType, + 'lean4.infoview.showTooltipOnHover': false, + 'lean4.input.leader': settings.abbreviationCharacter, + }, + }; + 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() - - _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) - - // Add a `Paste` option to the context menu on mobile. - // Monaco does not support clipboard pasting as all browsers block it - // due to security reasons. Therefore we use a codeMirror editor overlay - // which features good mobile support (but no Lean support yet) - if (mobile) { - leanMonacoEditor.editor?.addAction({ - id: "myPaste", - label: "Paste: open 'Plain Editor' for editing on mobile", - // keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V], - contextMenuGroupId: "9_cutcopypaste", - run: (_editor) => { - setCodeMirror(true) - } - }) - } - - // // TODO: This was an approach to create a new definition provider, but it - // // wasn't that useful. I'll leave it here in connection with the TODO below for - // // reference. - // monaco.languages.registerDefinitionProvider('lean4', { - // provideDefinition(model, position) { - // const word = model.getWordAtPosition(position); - // if (word) { - // console.log(`[Lean4web] Providing definition for: ${word.word}`); - // // Return the location of the definition - // return [ - // { - // uri: model.uri, - // range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range - // }, - // ]; - // } - // return null; - // }, - // }); - - // 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 - if (editorService) { - const openEditorBase = editorService.openCodeEditor.bind(editorService) - editorService.openCodeEditor = async (input: any, source: any) => { - 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 - // we try to create a doc-gen link from that. Could not extract the - // (fully-qualified) decalaration name... with that one could - // call `...${path}.html#${declaration}` - let path = input.resource.path.replace( - new RegExp("^.*/(?:lean|\.lake/packages/[^/]+/)"), "" - ).replace( - new RegExp("\.lean$"), "" - ) + 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); + await leanMonacoEditor.start( + editorRef.current!, + path.join(project, `${project}.lean`), + code ?? '', + ); + + 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 + // due to security reasons. Therefore we use a codeMirror editor overlay + // which features good mobile support (but no Lean support yet) + if (mobile) { + leanMonacoEditor.editor?.addAction({ + id: 'myPaste', + label: "Paste: open 'Plain Editor' for editing on mobile", + // keybindings: [monaco.KeyMod.CtrlCmd | monaco.KeyCode.KEY_V], + contextMenuGroupId: '9_cutcopypaste', + run: (_editor) => { + setCodeMirror(true); + }, + }); + } - if (window.confirm(`Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`)) { - let newTab = window.open(`https://leanprover-community.github.io/mathlib4_docs/${path}.html`, "_blank") - if (newTab) { - newTab.focus() - } - } + // // TODO: This was an approach to create a new definition provider, but it + // // wasn't that useful. I'll leave it here in connection with the TODO below for + // // reference. + // monaco.languages.registerDefinitionProvider('lean4', { + // provideDefinition(model, position) { + // const word = model.getWordAtPosition(position); + // if (word) { + // console.log(`[Lean4web] Providing definition for: ${word.word}`); + // // Return the location of the definition + // return [ + // { + // uri: model.uri, + // range: {startLineNumber: 0, startColumn: word.startColumn, endColumn: word.endColumn, endLineNumber: 0}, // Replace with actual definition range + // }, + // ]; + // } + // return null; + // }, + // }); + + // 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; + if (editorService) { + const openEditorBase = editorService.openCodeEditor.bind(editorService); + editorService.openCodeEditor = async (input: any, source: any) => { + 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 + // we try to create a doc-gen link from that. Could not extract the + // (fully-qualified) decalaration name... with that one could + // call `...${path}.html#${declaration}` + let path = input.resource.path + .replace(new RegExp('^.*/(?:lean|\.lake/packages/[^/]+/)'), '') + .replace(new RegExp('\.lean$'), ''); + + if ( + window.confirm( + `Do you want to open the docs?\n\n${path} (line ${input.options.selection.startLineNumber})`, + ) + ) { + let newTab = window.open( + `https://leanprover-community.github.io/mathlib4_docs/${path}.html`, + '_blank', + ); + if (newTab) { + newTab.focus(); } - return null - // return result // always return the base result + } } - } + 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()!) - }) - })() + // 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]) + 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 @@ -225,69 +239,75 @@ function App() { // 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}`) + if (!editor || !url) { + return; + } + console.debug(`[Lean4web] Loading from ${url}`); fetch(url) - .then((response) => response.text()) - .then((code) => { - setCodeFromUrl(code) - }) - .catch( err => { - let errorTxt = `ERROR: ${err.toString()}` - console.error(errorTxt) - setCodeFromUrl(errorTxt) - }) - }, [url, editor]) + .then((response) => response.text()) + .then((code) => { + setCodeFromUrl(code); + }) + .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 } - setContent(codeFromUrl) - }, [codeFromUrl]) + if (!codeFromUrl) { + return; + } + setContent(codeFromUrl); + }, [codeFromUrl]); // Keep the URL updated on change useEffect(() => { - if (!editor) { return } + if (!editor) { + return; + } - let _project = (project == 'MathlibDemo' ? null : project ?? null) + let _project = project == 'MathlibDemo' ? null : (project ?? null); let args: { - project: string | null - url: string | null - code: string | null - codez: string | null - } - if (code === "") { + project: string | null; + url: string | null; + code: string | null; + codez: string | null; + }; + if (code === '') { args = { project: _project, url: null, code: null, - codez: null - } + codez: null, + }; } else if (url != null && code == codeFromUrl) { args = { project: _project, url: encodeURIComponent(url), code: null, - codez: 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(/=*$/, '') + 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 - } + args = { + project: _project, + url: null, + code: null, + codez: compressed, + }; // } else { // args = { // project: _project, @@ -301,49 +321,52 @@ function App() { project: _project, url: null, code: fixedEncodeURIComponent(code), - codez: null - } + codez: null, + }; } - history.replaceState(undefined, undefined!, formatArgs(args)) - }, [editor, project, code, codeFromUrl]) + history.replaceState(undefined, undefined!, formatArgs(args)); + }, [editor, project, code, codeFromUrl]); // 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) - } - }, [code]) + const handleKeyUp = useCallback( + (event: KeyboardEvent) => { + if ((event.ctrlKey || event.metaKey) && event.key.toLowerCase() === 's') { + 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 (
@@ -359,53 +382,62 @@ function App() { restart={leanMonaco?.restart} codeMirror={codeMirror} setCodeMirror={setCodeMirror} - /> + /> - { - const gutter = document.createElement('div') - gutter.className = `gutter` // no `gutter-${direction}` as it might change - return gutter + const gutter = document.createElement('div'); + gutter.className = `gutter`; // no `gutter-${direction}` as it might change + return gutter; }} gutterStyle={(_dimension, gutterSize, _index) => { return { - 'width': mobile ? '100%' : `${gutterSize}px`, - 'height': mobile ? `${gutterSize}px` : '100%', - 'cursor': mobile ? 'row-resize' : 'col-resize', + width: mobile ? '100%' : `${gutterSize}px`, + height: mobile ? `${gutterSize}px` : '100%', + cursor: mobile ? 'row-resize' : 'col-resize', 'margin-left': mobile ? 0 : `-${gutterSize}px`, 'margin-top': mobile ? `-${gutterSize}px` : 0, 'z-index': 0, - }}} + }; + }} gutterSize={5} - onDragStart={() => setDragging(true)} onDragEnd={() => setDragging(false)} + onDragStart={() => setDragging(true)} + onDragEnd={() => setDragging(false)} sizes={mobile ? [50, 50] : [70, 30]} - direction={mobile ? "vertical" : "horizontal"} - style={{flexDirection: mobile ? "column" : "row"}}> -
- { codeMirror && + direction={mobile ? 'vertical' : 'horizontal'} + style={{ flexDirection: mobile ? 'column' : 'row' }} + > +
+ {codeMirror && ( - } + onChange={setContent} + /> + )}
-
-

- You are in the plain text editor

- Go back to the Monaco Editor (click ) - for the infoview to update! -

+
+

+ You are in the plain text editor +
+
+ Go back to the Monaco Editor (click ) for the infoview + to update! +

- ) + ); } -export default App +export default App; diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx index 655c306c..d9dc59bd 100644 --- a/client/src/Navigation.tsx +++ b/client/src/Navigation.tsx @@ -1,209 +1,313 @@ -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 { + 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 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' +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}) => { + 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} - -} + 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} + 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()}}/> - } - -} + {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
-
+ 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 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] + 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") + 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) - } + 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) - }} /> - ))} - - { + 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. + onClick={() => { + 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)}} /> - - -} + + { + 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}) => { +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) + 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 [privacyOpen, setPrivacyOpen] = useState(false); + const [impressumOpen, setImpressumOpen] = useState(false); + const [toolsOpen, setToolsOpen] = useState(false); + const [settingsOpen, setSettingsOpen] = useState(false); - const [mobile] = useAtom(mobileAtom) + 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) => { + 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) + setContent(codeFromUrl); } - return url - }) + return url; + }); if (project) { - setProject(project) + setProject(project); } - } + }; - const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails + const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails; - return
- { - setProject(ev.target.value) - console.log(`set Lean project to: ${ev.target.value}`) - }} > - {lean4webConfig.projects.map(proj => - + setProject(ev.target.value); + console.log(`set Lean project to: ${ev.target.value}`); + }} + > + {lean4webConfig.projects.map((proj) => ( + + ))} + + {mobile && ( + { + setCodeMirror(!codeMirror); + }} + /> )} - - { 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} /> -
-} + setLoadZulipOpen={setLoadZulipOpen} + /> + )} + { + 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 92cee746..00203ed9 100644 --- a/client/src/Popups/Impressum.tsx +++ b/client/src/Popups/Impressum.tsx @@ -1,24 +1,27 @@ -import { FC } from 'react' -import { Popup } from '../Navigation' -import lean4webConfig from '../config/config' +import { FC } from 'react'; +import { Popup } from '../Navigation'; +import lean4webConfig from '../config/config'; /** The popup with the privacy policy. */ const ImpressumPopup: FC<{ - open: boolean - handleClose: () => void -}> = ({open, handleClose}) => { - return -

Impressum

+ open: boolean; + handleClose: () => void; +}> = ({ open, handleClose }) => { + return ( + +

Impressum

- { lean4webConfig.contactDetails && -

- Contact details
- {lean4webConfig.contactDetails} -

- } + {lean4webConfig.contactDetails && ( +

+ Contact details +
+ {lean4webConfig.contactDetails} +

+ )} - { lean4webConfig.impressum } - -} + {lean4webConfig.impressum} + + ); +}; -export default ImpressumPopup +export default ImpressumPopup; diff --git a/client/src/Popups/LoadUrl.tsx b/client/src/Popups/LoadUrl.tsx index 0ac80283..e9c70d6b 100644 --- a/client/src/Popups/LoadUrl.tsx +++ b/client/src/Popups/LoadUrl.tsx @@ -1,37 +1,38 @@ -import { Popup } from '../Navigation' -import { FC, FormEvent, useRef, useState } from 'react' +import { Popup } from '../Navigation'; +import { FC, FormEvent, useRef, useState } from 'react'; const LoadUrlPopup: FC<{ - open: boolean - handleClose: () => void - loadFromUrl: (url: string) => void -}> = ({open, handleClose, loadFromUrl}) => { - + open: boolean; + handleClose: () => void; + loadFromUrl: (url: string) => void; +}> = ({ open, handleClose, loadFromUrl }) => { 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() - } + loadFromUrl(url); + handleClose(); + }; - return -

Load from URL

- {error ?

{error}

: null} -
- - -
- -} + return ( + +

Load from URL

+ {error ?

{error}

: null} +
+ + +
+ + ); +}; -export default LoadUrlPopup +export default LoadUrlPopup; diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx index 20eae0d9..471c5c3e 100644 --- a/client/src/Popups/LoadZulip.tsx +++ b/client/src/Popups/LoadZulip.tsx @@ -1,51 +1,62 @@ -import { Popup } from '../Navigation' -import { FC, FormEvent, useRef, useState } from 'react' +import { Popup } from '../Navigation'; +import { FC, FormEvent, useRef, useState } from 'react'; const LoadZulipPopup: FC<{ - open: boolean - handleClose: () => void - setContent: (code: string) => void -}> = ({open, handleClose, setContent}) => { - + open: boolean; + handleClose: () => void; + setContent: (code: string) => void; +}> = ({ open, handleClose, setContent }) => { const [error, setError] = useState(''); - const textInputRef = useRef(null) + 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]}).join('\n\n-- new codeblock\n\n').trim() + '\n' - setContent(code) + let code = + res + .map((s) => { + return s.match(regex2)![2]; + }) + .join('\n\n-- new codeblock\n\n') + .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 -

Link to Zulip message

-

Copy paste a zulip message here to extract - code-blocks. (mobile: "copy to clipboard", - web: "view message source") -

- {error ?

{error}

: null} -
-