From e019e7900cb5da78b69f95d438ab6bb69b41e7f0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 17:20:41 +0100 Subject: [PATCH 01/17] lint --- client/src/Navigation.tsx | 90 +++++++++++++++++------------ client/src/Popups/Impressum.tsx | 8 +-- client/src/Popups/LoadUrl.tsx | 10 +++- client/src/Popups/LoadZulip.tsx | 10 +++- client/src/Popups/PrivacyPolicy.tsx | 8 +-- client/src/Popups/Tools.tsx | 18 +++--- 6 files changed, 82 insertions(+), 62 deletions(-) diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx index d9dc59bd..bfdc252b 100644 --- a/client/src/Navigation.tsx +++ b/client/src/Navigation.tsx @@ -45,13 +45,19 @@ 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<{ +export function NavButton({ + icon, + iconElement, + text, + onClick = () => {}, + href = undefined, +}: { 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 ( @@ -59,10 +65,18 @@ export const NavButton: FC<{ {iconElement ?? } {text} ); -}; +} /** A button to appear in the hamburger menu or to navigation bar. */ -export const Dropdown: FC<{ +export function Dropdown({ + open, + setOpen, + icon, + text, + useOverlay = false, + onClick, + children, +}: { open: boolean; setOpen: Dispatch>; icon?: IconDefinition; @@ -70,7 +84,7 @@ export const Dropdown: FC<{ useOverlay?: boolean; onClick?: MouseEventHandler; children?: ReactNode; -}> = ({ open, setOpen, icon, text, useOverlay = false, onClick, children }) => { +}) { return ( <>
@@ -100,14 +114,18 @@ export const Dropdown: FC<{ )} ); -}; +} /** A popup which overlays the entire screen. */ -export const Popup: FC<{ +export function Popup({ + open, + handleClose, + children, +}: { open: boolean; handleClose: () => void; // TODO: what's the correct type? children?: ReactNode; -}> = ({ open, handleClose, children }) => { +}) { return (
@@ -117,21 +135,10 @@ export const Popup: FC<{
); -}; +} /** 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>; -}> = ({ +function FlexibleMenu({ isInDropdown = false, setOpenNav, openExample, @@ -142,7 +149,18 @@ const FlexibleMenu: FC<{ setContent, setLoadUrlOpen, setLoadZulipOpen, -}) => { +}: { + 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>; +}) { const loadFileFromDisk = (event: ChangeEvent) => { console.debug('Loading file from disk'); const fileToLoad = event.target.files![0]; @@ -225,20 +243,10 @@ const FlexibleMenu: FC<{ ); -}; +} /** 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>; -}> = ({ +export function Menu({ code, setContent, project, @@ -248,7 +256,17 @@ export const Menu: FC<{ restart, codeMirror, setCodeMirror, -}) => { +}: { + code: string; + setContent: (code: string) => void; + project: string; + setProject: Dispatch>; + setUrl: Dispatch>; + codeFromUrl: string; + restart?: () => void; + codeMirror: boolean; + setCodeMirror: Dispatch>; +}) { // state for handling the dropdown menus const [openNav, setOpenNav] = useState(false); const [openExample, setOpenExample] = useState(false); @@ -408,4 +426,4 @@ export const Menu: FC<{ />
); -}; +} diff --git a/client/src/Popups/Impressum.tsx b/client/src/Popups/Impressum.tsx index 00203ed9..e5db76f8 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'; /** 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

@@ -22,6 +18,6 @@ const ImpressumPopup: FC<{ {lean4webConfig.impressum} ); -}; +} export default ImpressumPopup; diff --git a/client/src/Popups/LoadUrl.tsx b/client/src/Popups/LoadUrl.tsx index e9c70d6b..e16ac111 100644 --- a/client/src/Popups/LoadUrl.tsx +++ b/client/src/Popups/LoadUrl.tsx @@ -1,11 +1,15 @@ import { Popup } from '../Navigation'; import { FC, FormEvent, useRef, useState } from 'react'; -const LoadUrlPopup: FC<{ +function LoadUrlPopup({ + open, + handleClose, + loadFromUrl, +}: { open: boolean; handleClose: () => void; loadFromUrl: (url: string) => void; -}> = ({ open, handleClose, loadFromUrl }) => { +}) { const [error, setError] = useState(''); const urlRef = useRef(null); @@ -33,6 +37,6 @@ const LoadUrlPopup: FC<{ ); -}; +} export default LoadUrlPopup; diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx index 471c5c3e..1a78c02c 100644 --- a/client/src/Popups/LoadZulip.tsx +++ b/client/src/Popups/LoadZulip.tsx @@ -1,11 +1,15 @@ import { Popup } from '../Navigation'; import { FC, FormEvent, useRef, useState } from 'react'; -const LoadZulipPopup: FC<{ +function LoadZulipPopup({ + open, + handleClose, + setContent, +}: { open: boolean; handleClose: () => void; setContent: (code: string) => void; -}> = ({ open, handleClose, setContent }) => { +}) { const [error, setError] = useState(''); const textInputRef = useRef(null); @@ -57,6 +61,6 @@ const LoadZulipPopup: FC<{ ); -}; +} export default LoadZulipPopup; diff --git a/client/src/Popups/PrivacyPolicy.tsx b/client/src/Popups/PrivacyPolicy.tsx index 95573766..a6ce2183 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'; /** 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

@@ -35,6 +31,6 @@ const PrivacyPopup: FC<{ )} ); -}; +} export default PrivacyPopup; diff --git a/client/src/Popups/Tools.tsx b/client/src/Popups/Tools.tsx index ff5b4cf3..a8b85bbc 100644 --- a/client/src/Popups/Tools.tsx +++ b/client/src/Popups/Tools.tsx @@ -1,5 +1,5 @@ import { Popup } from '../Navigation'; -import { FC, useEffect, useRef, useState } from 'react'; +import { useEffect, useRef, useState } from 'react'; // TODO: Do these interfaces exist somewhere in vscode-lean4? // They might need to be updated manually if changes to `lake` occur. @@ -68,9 +68,7 @@ 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 }) => { +function ToolTip({ pkg }: { pkg: LakePackage }) { const [loaded, setLoaded] = useState(false); const linkRef = useRef(null); const [commit, setCommit] = useState(); @@ -152,14 +150,18 @@ const ToolTip: FC<{ ); -}; +} /** Shows important information about the Lean project loaded in the web editor */ -const ToolsPopup: FC<{ +function ToolsPopup({ + open, + handleClose, + project, +}: { open: boolean; project: string; handleClose: () => void; -}> = ({ open, handleClose, project }) => { +}) { const [manifest, setManifest] = useState(emptyManifest); const [toolchain, setToolchain] = useState(''); // The last time `lake-manifest.json` has been modified @@ -260,6 +262,6 @@ const ToolsPopup: FC<{ ); -}; +} export default ToolsPopup; From caaa570d78a1e09b493889cc99ac70191a62b26a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 18:09:28 +0100 Subject: [PATCH 02/17] eslint --- .eslintrc.cjs | 18 - .vscode/settings.json | 15 +- client/src/.prettierrc.json | 2 +- client/src/App.tsx | 274 +- client/src/Navigation.tsx | 272 +- client/src/Popups/Impressum.tsx | 8 +- client/src/Popups/LoadUrl.tsx | 35 +- client/src/Popups/LoadZulip.tsx | 43 +- client/src/Popups/PrivacyPolicy.tsx | 8 +- client/src/Popups/Tools.tsx | 179 +- client/src/config/config.tsx | 6 +- client/src/config/docs.tsx | 22 +- client/src/index.tsx | 12 +- client/src/navigation/Dropdown.tsx | 53 + client/src/navigation/NavButton.tsx | 26 + client/src/settings/SettingsPopup.tsx | 74 +- client/src/settings/settings-atoms.ts | 63 +- client/src/settings/settings-types.ts | 32 +- .../src/settings/settings-url-converters.ts | 46 +- client/src/store/location-atoms.ts | 4 +- client/src/store/window-atoms.ts | 4 +- client/src/utils/Entries.ts | 4 +- client/src/utils/SaveToFile.tsx | 8 +- client/src/utils/UrlParsing.tsx | 28 +- client/src/utils/WindowWidth.tsx | 18 +- client/src/utils/cleanObject.ts | 2 +- client/src/utils/shallowEqual.ts | 4 +- client/src/vite-env.d.ts | 10 +- eslint.config.js | 61 + package-lock.json | 2252 ++++++++++++++++- package.json | 16 +- tsconfig.json | 2 +- vite.config.ts | 13 +- 33 files changed, 2883 insertions(+), 731 deletions(-) delete mode 100644 .eslintrc.cjs create mode 100644 client/src/navigation/Dropdown.tsx create mode 100644 client/src/navigation/NavButton.tsx create mode 100644 eslint.config.js 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/.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/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..f68587b2 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -1,107 +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 './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 LZString from 'lz-string' +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 { Menu } from './Navigation' +import { mobileAtom, settingsAtom, settingsUrlAtom } from './settings/settings-atoms' +import { lightThemes } from './settings/settings-types' +import { screenWidthAtom } from './store/window-atoms' +import { save } from './utils/SaveToFile' +import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing' /** 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: '' }, - }); + }) // 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); + 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))); + 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) + }, [setContent]) // 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; + return } - console.log('[Lean4web] Update lean4monaco options'); + 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 +128,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(); - - _leanMonaco.setInfoviewElement(infoviewRef.current!); - (async () => { - await _leanMonaco.start(options); + 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); + 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 +162,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 +190,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 +203,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,27 +213,27 @@ 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()!); - }); - })(); + setCode(leanMonacoEditor.editor?.getModel()?.getValue()!) + }) + })() return () => { - leanMonacoEditor.dispose(); - _leanMonaco.dispose(); - }; - }, [project, settings, options, infoviewRef, editorRef]); + leanMonacoEditor.dispose() + _leanMonaco.dispose() + } + }, [project, settings, options, infoviewRef, editorRef, code, mobile]) // Load content from source URL. // Once the editor is loaded, this reads the content of any provided `url=` in the URL and @@ -240,20 +242,20 @@ function App() { // changes, otherwise it might overwrite local changes too often. useEffect(() => { if (!editor || !url) { - return; + return } - console.debug(`[Lean4web] Loading from ${url}`); + console.debug(`[Lean4web] Loading from ${url}`) fetch(url) .then((response) => response.text()) .then((code) => { - setCodeFromUrl(code); + setCodeFromUrl(code) }) .catch((err) => { - let errorTxt = `ERROR: ${err.toString()}`; - console.error(errorTxt); - setCodeFromUrl(errorTxt); - }); - }, [url, editor]); + 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 @@ -261,42 +263,42 @@ function App() { // we would constantly overwrite the user's local changes useEffect(() => { if (!codeFromUrl) { - return; + return } - setContent(codeFromUrl); - }, [codeFromUrl]); + setContent(codeFromUrl) + }, [codeFromUrl]) // Keep the URL updated on change useEffect(() => { if (!editor) { - return; + 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; - }; + 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(/=*$/, ''); + 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) @@ -307,7 +309,7 @@ function App() { url: null, code: null, codez: compressed, - }; + } // } else { // args = { // project: _project, @@ -322,51 +324,51 @@ function App() { url: null, code: fixedEncodeURIComponent(code), codez: null, - }; + } } - history.replaceState(undefined, undefined!, formatArgs(args)); - }, [editor, project, code, codeFromUrl]); + history.replaceState(undefined, undefined!, formatArgs(args)) + }, [editor, project, code, codeFromUrl, url, settings.compress]) // 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); + 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 (
@@ -387,9 +389,9 @@ function App() { { - 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 { @@ -399,7 +401,7 @@ function App() { 'margin-left': mobile ? 0 : `-${gutterSize}px`, 'margin-top': mobile ? `-${gutterSize}px` : 0, 'z-index': 0, - }; + } }} gutterSize={5} onDragStart={() => setDragging(true)} @@ -437,7 +439,7 @@ function App() {
- ); + ) } -export default App; +export default App diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx index bfdc252b..d8988594 100644 --- a/client/src/Navigation.tsx +++ b/client/src/Navigation.tsx @@ -1,120 +1,36 @@ -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 './css/Modal.css' +import './css/Navigation.css' + +import { faArrowRotateRight, faCode, faInfoCircle } from '@fortawesome/free-solid-svg-icons' import { faArrowUpRightFromSquare, - faDownload, faBars, - faXmark, - faShield, - faHammer, + faCloudArrowUp, + faDownload, faGear, + faHammer, + faShield, 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 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} - - ); -} + faXmark, +} from '@fortawesome/free-solid-svg-icons' +import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' +import { useAtom } from 'jotai' +import { ChangeEvent, Dispatch, ReactNode, SetStateAction, useState } from 'react' -/** 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: Dispatch>; - 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(); - }} - /> - )} - - ); -} +import ZulipIcon from './assets/zulip.svg' +import lean4webConfig from './config/config' +import { Dropdown } from './navigation/Dropdown' +import { NavButton } from './navigation/NavButton' +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 { save } from './utils/SaveToFile' +import { lookupUrl } from './utils/UrlParsing' /** A popup which overlays the entire screen. */ export function Popup({ @@ -122,9 +38,9 @@ export function Popup({ handleClose, children, }: { - open: boolean; - handleClose: () => void; // TODO: what's the correct type? - children?: ReactNode; + open: boolean + handleClose: () => void // TODO: what's the correct type? + children?: ReactNode }) { return (
@@ -134,7 +50,7 @@ export function Popup({ {children}
- ); + ) } /** The menu items either appearing inside the dropdown or outside */ @@ -150,29 +66,29 @@ function FlexibleMenu({ setLoadUrlOpen, setLoadZulipOpen, }: { - 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: 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> }) { const loadFileFromDisk = (event: ChangeEvent) => { - console.debug('Loading file from disk'); - const fileToLoad = event.target.files![0]; - var fileReader = new FileReader(); + 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 ( <> @@ -183,8 +99,8 @@ function FlexibleMenu({ text="Examples" useOverlay={isInDropdown} onClick={() => { - setOpenLoad(false); - !isInDropdown && setOpenNav(false); + setOpenLoad(false) + !isInDropdown && setOpenNav(false) }} > {lean4webConfig.projects.map((proj) => @@ -197,8 +113,8 @@ function FlexibleMenu({ loadFromUrl( `${window.location.origin}/api/example/${proj.folder}/${example.file}`, proj.folder, - ); - setOpenExample(false); + ) + setOpenExample(false) }} /> )), @@ -211,8 +127,8 @@ function FlexibleMenu({ text="Load" useOverlay={isInDropdown} onClick={() => { - setOpenExample(false); - !isInDropdown && setOpenNav(false); + setOpenExample(false) + !isInDropdown && setOpenNav(false) }} > { - setLoadUrlOpen(true); + setLoadUrlOpen(true) }} /> } text="Load Zulip Message" onClick={() => { - setLoadZulipOpen(true); + setLoadZulipOpen(true) }} /> - ); + ) } /** The Navigation menu */ @@ -257,46 +173,46 @@ export function Menu({ codeMirror, setCodeMirror, }: { - code: string; - setContent: (code: string) => void; - project: string; - setProject: Dispatch>; - setUrl: Dispatch>; - codeFromUrl: string; - restart?: () => void; - codeMirror: boolean; - setCodeMirror: Dispatch>; + code: string + setContent: (code: string) => void + project: string + setProject: Dispatch> + setUrl: Dispatch> + codeFromUrl: string + restart?: () => void + codeMirror: boolean + setCodeMirror: Dispatch> }) { // 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'); + 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 (
@@ -304,8 +220,8 @@ export function Menu({ name="leanVersion" value={project} onChange={(ev) => { - setProject(ev.target.value); - console.log(`set Lean project to: ${ev.target.value}`); + setProject(ev.target.value) + console.log(`set Lean project to: ${ev.target.value}`) }} > {lean4webConfig.projects.map((proj) => ( @@ -319,7 +235,7 @@ export function Menu({ icon={faCode} text={codeMirror ? 'Lean' : 'Text'} onClick={() => { - setCodeMirror(!codeMirror); + setCodeMirror(!codeMirror) }} /> )} @@ -342,8 +258,8 @@ export function Menu({ setOpen={setOpenNav} icon={openNav ? faXmark : faBars} onClick={() => { - setOpenExample(false); - setOpenLoad(false); + setOpenExample(false) + setOpenLoad(false) }} > {mobile && ( @@ -364,7 +280,7 @@ export function Menu({ icon={faGear} text="Settings" onClick={() => { - setSettingsOpen(true); + setSettingsOpen(true) }} /> setToolsOpen(true)} /> @@ -374,7 +290,7 @@ export function Menu({ icon={faShield} text={'Privacy policy'} onClick={() => { - setPrivacyOpen(true); + setPrivacyOpen(true) }} /> {hasImpressum && ( @@ -382,7 +298,7 @@ export function Menu({ icon={faInfoCircle} text={'Impressum'} onClick={() => { - setImpressumOpen(true); + setImpressumOpen(true) }} /> )} @@ -425,5 +341,5 @@ export function Menu({ setContent={setContent} />
- ); + ) } diff --git a/client/src/Popups/Impressum.tsx b/client/src/Popups/Impressum.tsx index e5db76f8..539f8ae8 100644 --- a/client/src/Popups/Impressum.tsx +++ b/client/src/Popups/Impressum.tsx @@ -1,5 +1,5 @@ -import { Popup } from '../Navigation'; -import lean4webConfig from '../config/config'; +import lean4webConfig from '../config/config' +import { Popup } from '../Navigation' /** The popup with the privacy policy. */ function ImpressumPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) { @@ -17,7 +17,7 @@ function ImpressumPopup({ open, handleClose }: { open: boolean; handleClose: () {lean4webConfig.impressum} - ); + ) } -export default ImpressumPopup; +export default ImpressumPopup diff --git a/client/src/Popups/LoadUrl.tsx b/client/src/Popups/LoadUrl.tsx index e16ac111..14553221 100644 --- a/client/src/Popups/LoadUrl.tsx +++ b/client/src/Popups/LoadUrl.tsx @@ -1,31 +1,32 @@ -import { Popup } from '../Navigation'; -import { FC, FormEvent, useRef, useState } from 'react'; +import { FormEvent, useRef, useState } from 'react' + +import { Popup } from '../Navigation' function LoadUrlPopup({ open, handleClose, loadFromUrl, }: { - open: boolean; - handleClose: () => void; - loadFromUrl: (url: string) => void; + open: boolean + handleClose: () => void + loadFromUrl: (url: string) => void }) { - const [error, setError] = useState(''); - const urlRef = useRef(null); + 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 ( @@ -36,7 +37,7 @@ function LoadUrlPopup({ - ); + ) } -export default LoadUrlPopup; +export default LoadUrlPopup diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx index 1a78c02c..200fe607 100644 --- a/client/src/Popups/LoadZulip.tsx +++ b/client/src/Popups/LoadZulip.tsx @@ -1,46 +1,47 @@ -import { Popup } from '../Navigation'; -import { FC, FormEvent, useRef, useState } from 'react'; +import { FormEvent, useRef, useState } from 'react' + +import { Popup } from '../Navigation' function LoadZulipPopup({ open, handleClose, setContent, }: { - open: boolean; - handleClose: () => void; - setContent: (code: string) => void; + open: boolean + handleClose: () => void + setContent: (code: string) => void }) { - const [error, setError] = useState(''); - const textInputRef = useRef(null); + 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 ( @@ -60,7 +61,7 @@ function LoadZulipPopup({ - ); + ) } -export default LoadZulipPopup; +export default LoadZulipPopup diff --git a/client/src/Popups/PrivacyPolicy.tsx b/client/src/Popups/PrivacyPolicy.tsx index a6ce2183..c5f93841 100644 --- a/client/src/Popups/PrivacyPolicy.tsx +++ b/client/src/Popups/PrivacyPolicy.tsx @@ -1,5 +1,5 @@ -import { Popup } from '../Navigation'; -import lean4webConfig from '../config/config'; +import lean4webConfig from '../config/config' +import { Popup } from '../Navigation' /** The popup with the privacy policy. */ function PrivacyPopup({ open, handleClose }: { open: boolean; handleClose: () => void }) { @@ -30,7 +30,7 @@ function PrivacyPopup({ open, handleClose }: { open: boolean; handleClose: () =>

)} - ); + ) } -export default PrivacyPopup; +export default PrivacyPopup diff --git a/client/src/Popups/Tools.tsx b/client/src/Popups/Tools.tsx index a8b85bbc..91e3eee7 100644 --- a/client/src/Popups/Tools.tsx +++ b/client/src/Popups/Tools.tsx @@ -1,36 +1,37 @@ -import { Popup } from '../Navigation'; -import { useEffect, useRef, useState } from 'react'; +import { useEffect, useRef, useState } from 'react' + +import { Popup } from '../Navigation' // 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 @@ -69,59 +70,59 @@ interface CommitInfo { * rarely used feature, it might be fine for now. */ function ToolTip({ pkg }: { pkg: LakePackage }) { - 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]); + 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 ( @@ -149,7 +150,7 @@ function ToolTip({ pkg }: { pkg: LakePackage }) { )} - ); + ) } /** Shows important information about the Lean project loaded in the web editor */ @@ -158,48 +159,48 @@ function ToolsPopup({ handleClose, project, }: { - open: boolean; - project: string; - handleClose: () => void; + open: boolean + project: string + handleClose: () => void }) { - const [manifest, setManifest] = useState(emptyManifest); - const [toolchain, setToolchain] = useState(''); + 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 ( @@ -261,7 +262,7 @@ function ToolsPopup({ #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/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/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index a34eac48..6a0f1451 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -1,14 +1,14 @@ -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' +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, @@ -17,27 +17,27 @@ export function SettingsPopup({ project, setProject, }: { - open: boolean; - handleClose: () => void; - closeNav: () => void; - project: string; - setProject: (project: string) => void; + open: boolean + handleClose: () => void + closeNav: () => void + project: string + setProject: (project: string) => 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 +67,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 +76,7 @@ export function SettingsPopup({ { - updateSetting('wordWrap', !newSettings.wordWrap); + updateSetting('wordWrap', !newSettings.wordWrap) }} checked={newSettings.wordWrap} /> @@ -86,7 +86,7 @@ export function SettingsPopup({ { - updateSetting('acceptSuggestionOnEnter', !newSettings.acceptSuggestionOnEnter); + updateSetting('acceptSuggestionOnEnter', !newSettings.acceptSuggestionOnEnter) }} checked={newSettings.acceptSuggestionOnEnter} /> @@ -96,7 +96,7 @@ export function SettingsPopup({ { - updateSetting('showGoalNames', !newSettings.showGoalNames); + updateSetting('showGoalNames', !newSettings.showGoalNames) }} checked={newSettings.showGoalNames} /> @@ -106,7 +106,7 @@ export function SettingsPopup({ { - updateSetting('showExpectedType', !newSettings.showExpectedType); + updateSetting('showExpectedType', !newSettings.showExpectedType) }} checked={newSettings.showExpectedType} /> @@ -121,7 +121,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 +145,7 @@ export function SettingsPopup({ '& .MuiSlider-track': { display: 'none' }, }} onChange={(_, val) => { - updateSetting('mobile', mobileSliderMarks[val].key); + updateSetting('mobile', mobileSliderMarks[val].key) }} /> @@ -154,7 +154,7 @@ export function SettingsPopup({ { - updateSetting('compress', !newSettings.compress); + updateSetting('compress', !newSettings.compress) }} checked={newSettings.compress} /> @@ -164,7 +164,7 @@ export function SettingsPopup({ { - updateSetting('inUrl', !newSettings.inUrl); + updateSetting('inUrl', !newSettings.inUrl) }} checked={newSettings.inUrl} /> @@ -178,7 +178,7 @@ export function SettingsPopup({ { - updateSetting('saved', !newSettings.saved); + updateSetting('saved', !newSettings.saved) }} checked={newSettings.saved} /> @@ -189,8 +189,8 @@ export function SettingsPopup({