From 31ef44fa24b11678ddbb4743035367a072714ceb Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 03:55:55 +0100 Subject: [PATCH 1/5] settings in URL --- .eslintrc.cjs | 7 +- client/src/App.tsx | 15 ++-- client/src/settings/SettingsPopup.tsx | 29 +++---- client/src/settings/settings-atoms.ts | 63 ++++++++++----- client/src/settings/settings-types.ts | 110 ++++++++++++++++++-------- client/src/store/location-atoms.ts | 3 + client/src/utils/cleanObject.ts | 6 ++ doc/Usage.md | 14 ++-- package-lock.json | 11 +++ package.json | 1 + tsconfig.json | 29 +++---- 11 files changed, 184 insertions(+), 104 deletions(-) create mode 100644 client/src/store/location-atoms.ts create mode 100644 client/src/utils/cleanObject.ts diff --git a/.eslintrc.cjs b/.eslintrc.cjs index d6c95379..81b15e1a 100644 --- a/.eslintrc.cjs +++ b/.eslintrc.cjs @@ -9,10 +9,5 @@ module.exports = { ignorePatterns: ['dist', '.eslintrc.cjs'], parser: '@typescript-eslint/parser', plugins: ['react-refresh'], - rules: { - 'react-refresh/only-export-components': [ - 'warn', - { allowConstantExport: true }, - ], - }, + rules: {}, } diff --git a/client/src/App.tsx b/client/src/App.tsx index 91617e01..63d5ab81 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -20,9 +20,10 @@ import { useWindowDimensions } from './utils/WindowWidth' // CSS import './css/App.css' import './css/Editor.css' -import { mobileAtom, settingsAtom } from './settings/settings-atoms' +import { mobileAtom, settingsAtom, settingsUrlAtom } from './settings/settings-atoms' import { useAtom } from 'jotai/react' import { screenWidthAtom } from './store/window-atoms' +import { locationAtom } from './store/location-atoms' /** Returns true if the browser wants dark mode */ function isBrowserDefaultDark() { @@ -38,7 +39,7 @@ function App() { const [settings] = useAtom(settingsAtom) const [mobile] = useAtom(mobileAtom) const [, setScreenWidth] = useAtom(screenWidthAtom) - const { width } = useWindowDimensions() + const [searchParams] = useAtom(settingsUrlAtom) // Lean4monaco options const [options, setOptions] = useState({ @@ -54,7 +55,7 @@ function App() { // the user data const [code, setCode] = useState('') - const [project, setProject] = useState(undefined) + const [project, setProject] = useState() const [url, setUrl] = useState(null) const [codeFromUrl, setCodeFromUrl] = useState('') @@ -64,6 +65,10 @@ function App() { setCode(code) } + useEffect(() => { + console.debug("location:",searchParams) + }, [searchParams]) + // Read the URL arguments useEffect(() => { // Parse args @@ -132,7 +137,7 @@ function App() { // Setting up the editor and infoview useEffect(() => { - // if (project === undefined) return + if (project === undefined) return console.debug('[Lean4web] Restarting editor') var _leanMonaco = new LeanMonaco() var leanMonacoEditor = new LeanMonacoEditor() @@ -257,7 +262,7 @@ function App() { useEffect(() => { if (!editor) { return } - let _project = (project == 'MathlibDemo' ? null : project) + let _project = (project == 'MathlibDemo' ? null : project ?? null) let args: { project: string | null url: string | null diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index 1409f6ae..851657d9 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -1,12 +1,10 @@ import { Dispatch, FC, SetStateAction, createContext, useContext, useState } from 'react' import Switch from '@mui/material/Switch'; -import lean4webConfig from '../config/config' import { Popup } from '../Navigation'; import { defaultSettings, Settings } from './settings-types' import type { MobileValues, Theme } from './settings-types' -import { applyAndSaveSettingsAtom, applySettingsAtom, hasSettingsSavedAtom, mobileAtom, settingsAtom } from './settings-atoms'; +import { applySettingsAtom, settingsAtom } from './settings-atoms'; import { useAtom } from 'jotai/react'; -import FormControlLabel from '@mui/material/FormControlLabel'; import Slider from '@mui/material/Slider'; import Box from '@mui/material/Box'; @@ -66,12 +64,9 @@ const SettingsPopup: FC<{ project: string setProject: Dispatch> }> = ({open, handleClose, closeNav, project, setProject}) => { - const [hasSettingsSaved] = useAtom(hasSettingsSavedAtom) const [settings, setSettings] = useAtom(settingsAtom) - const [, applyAndSaveStore] = useAtom(applyAndSaveSettingsAtom) - const [, applyAndClearStore] = useAtom(applySettingsAtom) + const [, applySettings] = useAtom(applySettingsAtom) const [newSettings, setNewSettings] = useState(settings) - const [allowSaveInStore, setAllowSaveInStore] = useState(hasSettingsSaved) function updateSetting(key: K, value: Settings[K]) { setNewSettings(prev => ({ ...prev, [key]: value })) @@ -143,7 +138,7 @@ const SettingsPopup: FC<{ Layout: item.key === newSettings.mobile).value} + value={marks.find(item => item.key === newSettings.mobile)?.value ?? 1} step={1} marks={marks} max={2} @@ -165,24 +160,22 @@ const SettingsPopup: FC<{

Save

Editor settings and User settings are not preserved unless you opt-in to save them.

- {setAllowSaveInStore(prev => !prev)}} checked={allowSaveInStore} /> + {updateSetting("saved", !newSettings.saved)}} checked={newSettings.saved} />

+

+ {updateSetting("inUrl", !newSettings.inUrl)}} checked={newSettings.inUrl} /> + +

{newSettings != defaultSettings && - + } { - if (allowSaveInStore) { - applyAndSaveStore(newSettings) - } else { - applyAndClearStore(newSettings) - } - }}/> + value={newSettings.saved ? "Apply & Save" : "Apply"} + onClick={() => applySettings(newSettings)}/>

diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index 915ad758..c27941bc 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -1,37 +1,58 @@ import { atomWithStorage, createJSONStorage } from 'jotai/utils' -import { defaultSettings, Settings, SettingsStore } from './settings-types' +import { decodeSettingsFromURL, defaultSettings, encodeSettingsToURL, Settings, SettingsStore, Theme } from './settings-types' import { atom } from 'jotai/vanilla' import { screenWidthAtom } from '../store/window-atoms' - -/** The settings which apply for the current session */ -const settingsBaseAtom = atom(defaultSettings) +import { locationAtom } from '../store/location-atoms' +import { cleanObject } from '../utils/cleanObject' /** User settings as they are stored in storage */ -const settingsStoreAtom = atomWithStorage('lean4web:settings', undefined, undefined, { getOnInit: true }) +const settingsStoreAtom = atomWithStorage('lean4web:settings', {}, undefined, { getOnInit: true }) + +/** The settings which are set in the searchParams of the opened URL */ +export const settingsUrlAtom = atom(get => { + const searchParams = get(locationAtom).searchParams + if (!searchParams) return {} + return decodeSettingsFromURL(searchParams) +}) + +/** The settings which apply for the current session */ +const settingsBaseAtom = atom({saved: false, inUrl: false, ...defaultSettings}) -/** The user settings */ +/** + * The user settings combined from different sources, with decreasing priority: + * - url params + * - browser storage + * - current (local) state (base) + * - default values (base) + */ export const settingsAtom = atom(get => { const base = get(settingsBaseAtom) - const store = get(settingsStoreAtom) - return { ...base, ...store } as Settings + const store = cleanObject(get(settingsStoreAtom)) + const url = cleanObject(get(settingsUrlAtom)) + return { + ...base, + ...store, + ...url, + saved: Object.entries(store).length > 0, + inUrl: Object.entries(url).length > 0, + } as Settings }) -/** Set the new settings and save the to local storage */ -export const applyAndSaveSettingsAtom = atom(null, (get, set, val) => { - set(settingsBaseAtom, val) - set(settingsStoreAtom, val) -}) +/** Set the new settings, and write them to browser storage or URL if desired */ +export const applySettingsAtom = atom(null, (get, set, val: Settings) => { + const { saved, inUrl, ...settingsToStore } = val; -/** Set the new settings without saving to local storage */ -export const applySettingsAtom = atom(null, (get, set, val) => { set(settingsBaseAtom, val) - localStorage.removeItem('lean4web:settings') -}) -/** Indicates if there are saved settings in storage */ -export const hasSettingsSavedAtom = atom(get => { - const store = get(settingsStoreAtom) - return store !== undefined + if (saved) { + set(settingsStoreAtom, settingsToStore) + } else { + localStorage.removeItem('lean4web:settings') + } + + const newSearchParams = inUrl ? encodeSettingsToURL(settingsToStore) : new URLSearchParams() + const location = get(locationAtom) + set(locationAtom, { ...location, searchParams: newSearchParams}) }) /** Indicates whether mobile layout should be used */ diff --git a/client/src/settings/settings-types.ts b/client/src/settings/settings-types.ts index 9005a7b5..a2883298 100644 --- a/client/src/settings/settings-types.ts +++ b/client/src/settings/settings-types.ts @@ -1,16 +1,10 @@ -/* -This file contains the default settings for settings that can be changed by the user. - -Note that more Editor options are set in `App.tsx` directly. -*/ - // const isBrowserDefaultDark = () => window.matchMedia('(prefers-color-scheme: dark)').matches export type Theme = "Visual Studio Light" | "Visual Studio Dark" | "Default High Contrast" | "Cobalt" export type MobileValues = boolean | "auto" -/** Type for the user settings. */ +/** Type for the settings, including internal ones */ export interface Settings { /** Lead character to trigger unicode input mode */ abbreviationCharacter: string @@ -29,43 +23,27 @@ export interface Settings { theme: Theme, /** Wrap code */ wordWrap: boolean - saveInLocalStorage: boolean + // internal: saved to browser storage + saved: boolean + // internal: written to search params + inUrl: boolean } -/** Same as `Settings` but everything is optional, since single keys might be missing in the browser store */ -export interface SettingsStore { - abbreviationCharacter?: string - acceptSuggestionOnEnter?: boolean - showGoalNames?: boolean - compress?: boolean, - mobile?: MobileValues - theme?: Theme, - wordWrap?: boolean - saveInLocalStorage?: boolean -} +/** The settings which are not internal */ +export type UserSettings = Omit -export const preferenceParams: (keyof Settings)[] = [ - "abbreviationCharacter", - "acceptSuggestionOnEnter", - // "compress", // not sure if this should be user-settable - "showGoalNames", - "mobile", - "theme", - "wordWrap", -] +/** Same as `UserSettings` but everything is optional, since single keys might be missing in the browser store */ +export type SettingsStore = Partial /** The default settings. */ -export const defaultSettings: Settings = { +export const defaultSettings: UserSettings = { abbreviationCharacter: '\\', acceptSuggestionOnEnter: false, showGoalNames: true, compress: true, - /** value likely overwritten with `width < 800` in App.tsx - * unless provided in URL searchparams or in local storage. */ mobile: "auto", theme: 'Visual Studio Light', // irrelevant as it will be overwritten in App.tsx wordWrap: true, - saveInLocalStorage: false, } /** @@ -77,3 +55,71 @@ export const lightThemes: Theme[] = [ 'Visual Studio Light' ] +export function decodeSettingsFromURL(searchParams: URLSearchParams): SettingsStore { + return { + abbreviationCharacter: searchParams.get('abbreviationCharacter') ?? undefined, + acceptSuggestionOnEnter: parseBooleanSearchParam(searchParams, 'acceptSuggestionOnEnter'), + mobile: parseBooleanSearchParam(searchParams, 'mobile'), + compress: parseBooleanSearchParam(searchParams, 'compress'), + showGoalNames: parseBooleanSearchParam(searchParams, 'showGoalNames'), + theme: decodeTheme(searchParams.get("theme") ?? undefined), + wordWrap: parseBooleanSearchParam(searchParams, 'wordWrap'), + } +} + +function decodeTheme(val?: string): Theme | undefined { + if (val === undefined) return + switch (val.toLowerCase()) { + case "light": + return "Visual Studio Light" + break + case "dark": + return "Visual Studio Dark" + break + default: + console.warn(`expected search param 'theme' to be 'light' or 'dark'.`) + } +} + +function parseBooleanSearchParam(searchParams: URLSearchParams, name: string) { + const param = searchParams.get(name) ?? undefined + return convertToBoolean(name,param) +} + +/** `name` is only used for the error message */ +function convertToBoolean(name: string, val?: string) { + if (val === undefined) return + switch (val.toLowerCase()) { + case "true": + return true + case "false": + return false + default: + console.warn(`expected search param '${name}' to be 'true' or 'false'.`) + } +} + +export function encodeSettingsToURL(val: UserSettings): URLSearchParams { + const searchParams = new URLSearchParams() + Object.entries(val) + .filter(([_, v]) => v !== undefined) + .forEach(([key, v]) => { + setParam(searchParams, key as keyof UserSettings, v) + }) + return searchParams +} + +function setParam(searchParams: URLSearchParams, key: K, value: UserSettings[K]) { + switch (key) { + case "theme": + searchParams.set(String(key), lightThemes.includes(value as Theme) ? "light" : "dark") + break + case "mobile": + if (value !== "auto") { + searchParams.set(String(key), String(value as Boolean)) + } + break + default: + searchParams.set(String(key), String(value)) + } +} diff --git a/client/src/store/location-atoms.ts b/client/src/store/location-atoms.ts new file mode 100644 index 00000000..8acded4c --- /dev/null +++ b/client/src/store/location-atoms.ts @@ -0,0 +1,3 @@ +import { atomWithLocation } from 'jotai-location' + +export const locationAtom = atomWithLocation() diff --git a/client/src/utils/cleanObject.ts b/client/src/utils/cleanObject.ts new file mode 100644 index 00000000..cbe253b2 --- /dev/null +++ b/client/src/utils/cleanObject.ts @@ -0,0 +1,6 @@ +/** Removes all keys which have `undefined` as value */ +export function cleanObject(obj: T): Partial { + return Object.fromEntries( + Object.entries(obj).filter(([_, v]) => v !== undefined) + ) as Partial; +} diff --git a/doc/Usage.md b/doc/Usage.md index 22bd52fc..b5434b59 100644 --- a/doc/Usage.md +++ b/doc/Usage.md @@ -33,9 +33,11 @@ When a setting is not provided as URL parameter, the value from the browser stor The recognised settings are: -- `abbreviationCharacter`: Leader character to type to introduce abbrevations, default is `\` -- `acceptSuggestionOnEnter`: Accept code editors suggestions on Enter, default is false -- `showGoalNames`: Show goal names in Lean infoview box, default is true -- `mobile`: Display code editor and infoview in narrow, vertically stacked, mobile-friendly mode. Usually inferred from window width. -- `theme`: `light` or `dark`. Usually inferred from browser dark mode preferences. -- `wordWrap`: Wrap code in editor box, default is true +- Boolean settings (`true` or `false`): + - `acceptSuggestionOnEnter`: accept code editors suggestions on `Enter`. default: `false` + - `showGoalNames`: show goal names in Lean infoview box. default: `true` + - `mobile`: display code editor and infoview in narrow, vertically stacked, mobile-friendly mode. default: not set, i.e. inferred + - `wordWrap`: wrap code in editor box. default: `true` +- Non-boolean settings: +- `abbreviationCharacter`: lead character for unicode abbreviations. values: a character. default: `\` +- `theme`: selection between one light and dark theme. More themes are available in the settings, but they cannot be set through the URL. values: `light` or `dark`. default: `light` (TODO: infererred from browser) diff --git a/package-lock.json b/package-lock.json index 2d951630..6ab9c973 100644 --- a/package-lock.json +++ b/package-lock.json @@ -19,6 +19,7 @@ "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", "jotai": "^2.16.1", + "jotai-location": "^0.6.2", "jotai-react": "^0.0.0", "lean4monaco": "^1.1.4", "lz-string": "^1.5.0", @@ -6385,6 +6386,7 @@ "resolved": "https://registry.npmjs.org/jotai/-/jotai-2.16.1.tgz", "integrity": "sha512-vrHcAbo3P7Br37C8Bv6JshMtlKMPqqmx0DDREtTjT4nf3QChDrYdbH+4ik/9V0cXA57dK28RkJ5dctYvavcIlg==", "license": "MIT", + "peer": true, "engines": { "node": ">=12.20.0" }, @@ -6409,6 +6411,15 @@ } } }, + "node_modules/jotai-location": { + "version": "0.6.2", + "resolved": "https://registry.npmjs.org/jotai-location/-/jotai-location-0.6.2.tgz", + "integrity": "sha512-D+fqGNNgPHpehOsGBsYsS7F3kNgml099MJrGYt8YlLumcnoTVrBdcO+Y11KyMlyzwPihEN0HPUgke9Iihz9OXw==", + "license": "MIT", + "peerDependencies": { + "jotai": ">=1.11.0" + } + }, "node_modules/jotai-react": { "version": "0.0.0", "resolved": "https://registry.npmjs.org/jotai-react/-/jotai-react-0.0.0.tgz", diff --git a/package.json b/package.json index 297506a2..3ae2e456 100644 --- a/package.json +++ b/package.json @@ -41,6 +41,7 @@ "file-saver": "^2.0.5", "ip-anonymize": "^0.1.0", "jotai": "^2.16.1", + "jotai-location": "^0.6.2", "jotai-react": "^0.0.0", "lean4monaco": "^1.1.4", "lz-string": "^1.5.0", diff --git a/tsconfig.json b/tsconfig.json index 14236936..e84daf92 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -1,13 +1,10 @@ { "compilerOptions": { "outDir": "./client/dist/", - "composite": true, - "tsBuildInfoFile": "./node_modules/.tmp/tsconfig.app.tsbuildinfo", - "target": "ES2020", + "target": "ES2023", "useDefineForClassFields": true, - "lib": ["ES2020", "DOM", "DOM.Iterable"], + "lib": ["ES2023", "DOM", "DOM.Iterable"], "module": "ESNext", - "skipLibCheck": true, /* Bundler mode */ "moduleResolution": "bundler", @@ -18,15 +15,15 @@ "noEmit": true, "jsx": "react-jsx", - /* Linting */ - // "strict": true, - // "noUnusedLocals": true, - // "noUnusedParameters": true, - // "noFallthroughCasesInSwitch": true + /* Type Safety */ + "strict": true, + "noFallthroughCasesInSwitch": true, + "noUnusedLocals": false, + "noUnusedParameters": false, + + /* Performance */ + "skipLibCheck": true }, - // "include": ["client/src"] - "exclude": [ - "server", - "node_modules" - ] -} + "include": ["client/src"], + "exclude": ["server", "node_modules"] +} \ No newline at end of file From cbe7a83edeaea4c8dbb2235c0ad837ef55167348 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 04:22:50 +0100 Subject: [PATCH 2/5] cleanup --- client/src/App.tsx | 6 +- client/src/settings/SettingsPopup.tsx | 5 ++ client/src/settings/settings-atoms.ts | 7 +- client/src/settings/settings-types.ts | 76 ++----------------- .../src/settings/settings-url-converters.ts | 71 +++++++++++++++++ doc/Usage.md | 4 +- 6 files changed, 91 insertions(+), 78 deletions(-) create mode 100644 client/src/settings/settings-url-converters.ts diff --git a/client/src/App.tsx b/client/src/App.tsx index 63d5ab81..32b93bda 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -55,7 +55,7 @@ function App() { // the user data const [code, setCode] = useState('') - const [project, setProject] = useState() + const [project, setProject] = useState('MathlibDemo') const [url, setUrl] = useState(null) const [codeFromUrl, setCodeFromUrl] = useState('') @@ -85,7 +85,7 @@ function App() { 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) @@ -127,7 +127,7 @@ function App() { "lean4.input.eagerReplacementEnabled": true, "lean4.infoview.showGoalNames": settings.showGoalNames, "lean4.infoview.emphasizeFirstGoal": true, - "lean4.infoview.showExpectedType": false, + "lean4.infoview.showExpectedType": settings.showExpectedType, "lean4.infoview.showTooltipOnHover": false, "lean4.input.leader": settings.abbreviationCharacter } diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index 851657d9..988a53a6 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -114,6 +114,11 @@ const SettingsPopup: FC<{ checked={newSettings.showGoalNames} />

+

+ {updateSetting("showExpectedType", !newSettings.showExpectedType)}} + checked={newSettings.showExpectedType} /> + +

User settings

diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index c27941bc..badf27d0 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -1,15 +1,16 @@ import { atomWithStorage, createJSONStorage } from 'jotai/utils' -import { decodeSettingsFromURL, defaultSettings, encodeSettingsToURL, Settings, SettingsStore, Theme } from './settings-types' +import { defaultSettings, Settings, PartialUserSettings, Theme } from './settings-types' import { atom } from 'jotai/vanilla' import { screenWidthAtom } from '../store/window-atoms' import { locationAtom } from '../store/location-atoms' import { cleanObject } from '../utils/cleanObject' +import { decodeSettingsFromURL, encodeSettingsToURL } from './settings-url-converters' /** User settings as they are stored in storage */ -const settingsStoreAtom = atomWithStorage('lean4web:settings', {}, undefined, { getOnInit: true }) +const settingsStoreAtom = atomWithStorage('lean4web:settings', {}, undefined, { getOnInit: true }) /** The settings which are set in the searchParams of the opened URL */ -export const settingsUrlAtom = atom(get => { +export const settingsUrlAtom = atom(get => { const searchParams = get(locationAtom).searchParams if (!searchParams) return {} return decodeSettingsFromURL(searchParams) diff --git a/client/src/settings/settings-types.ts b/client/src/settings/settings-types.ts index a2883298..ed921421 100644 --- a/client/src/settings/settings-types.ts +++ b/client/src/settings/settings-types.ts @@ -12,6 +12,8 @@ export interface Settings { acceptSuggestionOnEnter: boolean /** Show goal names in Lean infoview box */ showGoalNames: boolean + /** Show expected type in Lean infoview box */ + showExpectedType: boolean /** Compress the `code=` in the URL into `codez=` using LZ-string */ compress: boolean, /** Display code editor and infoview in narrow, vertically stacked, mobile-friendly mode. @@ -33,16 +35,17 @@ export interface Settings { export type UserSettings = Omit /** Same as `UserSettings` but everything is optional, since single keys might be missing in the browser store */ -export type SettingsStore = Partial +export type PartialUserSettings = Partial /** The default settings. */ export const defaultSettings: UserSettings = { abbreviationCharacter: '\\', acceptSuggestionOnEnter: false, showGoalNames: true, + showExpectedType: false, compress: true, mobile: "auto", - theme: 'Visual Studio Light', // irrelevant as it will be overwritten in App.tsx + theme: 'Visual Studio Light', // TODO: introduce "auto" which takes the browser setting. wordWrap: true, } @@ -54,72 +57,3 @@ export const defaultSettings: UserSettings = { export const lightThemes: Theme[] = [ 'Visual Studio Light' ] - -export function decodeSettingsFromURL(searchParams: URLSearchParams): SettingsStore { - return { - abbreviationCharacter: searchParams.get('abbreviationCharacter') ?? undefined, - acceptSuggestionOnEnter: parseBooleanSearchParam(searchParams, 'acceptSuggestionOnEnter'), - mobile: parseBooleanSearchParam(searchParams, 'mobile'), - compress: parseBooleanSearchParam(searchParams, 'compress'), - showGoalNames: parseBooleanSearchParam(searchParams, 'showGoalNames'), - theme: decodeTheme(searchParams.get("theme") ?? undefined), - wordWrap: parseBooleanSearchParam(searchParams, 'wordWrap'), - } -} - -function decodeTheme(val?: string): Theme | undefined { - if (val === undefined) return - switch (val.toLowerCase()) { - case "light": - return "Visual Studio Light" - break - case "dark": - return "Visual Studio Dark" - break - default: - console.warn(`expected search param 'theme' to be 'light' or 'dark'.`) - } -} - -function parseBooleanSearchParam(searchParams: URLSearchParams, name: string) { - const param = searchParams.get(name) ?? undefined - return convertToBoolean(name,param) -} - -/** `name` is only used for the error message */ -function convertToBoolean(name: string, val?: string) { - if (val === undefined) return - switch (val.toLowerCase()) { - case "true": - return true - case "false": - return false - default: - console.warn(`expected search param '${name}' to be 'true' or 'false'.`) - } -} - -export function encodeSettingsToURL(val: UserSettings): URLSearchParams { - const searchParams = new URLSearchParams() - Object.entries(val) - .filter(([_, v]) => v !== undefined) - .forEach(([key, v]) => { - setParam(searchParams, key as keyof UserSettings, v) - }) - return searchParams -} - -function setParam(searchParams: URLSearchParams, key: K, value: UserSettings[K]) { - switch (key) { - case "theme": - searchParams.set(String(key), lightThemes.includes(value as Theme) ? "light" : "dark") - break - case "mobile": - if (value !== "auto") { - searchParams.set(String(key), String(value as Boolean)) - } - break - default: - searchParams.set(String(key), String(value)) - } -} diff --git a/client/src/settings/settings-url-converters.ts b/client/src/settings/settings-url-converters.ts new file mode 100644 index 00000000..fb040051 --- /dev/null +++ b/client/src/settings/settings-url-converters.ts @@ -0,0 +1,71 @@ +import { lightThemes, PartialUserSettings, Theme, UserSettings } from "./settings-types" + +export function decodeSettingsFromURL(searchParams: URLSearchParams): PartialUserSettings { + return { + abbreviationCharacter: searchParams.get('abbreviationCharacter') ?? undefined, + acceptSuggestionOnEnter: parseBooleanSearchParam(searchParams, 'acceptSuggestionOnEnter'), + mobile: parseBooleanSearchParam(searchParams, 'mobile'), + compress: parseBooleanSearchParam(searchParams, 'compress'), + showGoalNames: parseBooleanSearchParam(searchParams, 'showGoalNames'), + showExpectedType: parseBooleanSearchParam(searchParams, 'showExpectedType'), + theme: decodeTheme(searchParams.get("theme") ?? undefined), + wordWrap: parseBooleanSearchParam(searchParams, 'wordWrap'), + } +} + +function decodeTheme(val?: string): Theme | undefined { + if (val === undefined) return + switch (val.toLowerCase()) { + case "light": + return "Visual Studio Light" + break + case "dark": + return "Visual Studio Dark" + break + default: + console.warn(`expected search param 'theme' to be 'light' or 'dark'.`) + } +} + +function parseBooleanSearchParam(searchParams: URLSearchParams, name: string) { + const param = searchParams.get(name) ?? undefined + return convertToBoolean(name,param) +} + +/** `name` is only used for the error message */ +function convertToBoolean(name: string, val?: string) { + if (val === undefined) return + switch (val.toLowerCase()) { + case "true": + return true + case "false": + return false + default: + console.warn(`expected search param '${name}' to be 'true' or 'false'.`) + } +} + +export function encodeSettingsToURL(val: UserSettings): URLSearchParams { + const searchParams = new URLSearchParams() + Object.entries(val) + .filter(([_, v]) => v !== undefined) + .forEach(([key, v]) => { + setParam(searchParams, key as keyof UserSettings, v) + }) + return searchParams +} + +function setParam(searchParams: URLSearchParams, key: K, value: UserSettings[K]) { + switch (key) { + case "theme": + searchParams.set(String(key), lightThemes.includes(value as Theme) ? "light" : "dark") + break + case "mobile": + if (value !== "auto") { + searchParams.set(String(key), String(value as Boolean)) + } + break + default: + searchParams.set(String(key), String(value)) + } +} diff --git a/doc/Usage.md b/doc/Usage.md index b5434b59..dc978a24 100644 --- a/doc/Usage.md +++ b/doc/Usage.md @@ -35,8 +35,10 @@ The recognised settings are: - Boolean settings (`true` or `false`): - `acceptSuggestionOnEnter`: accept code editors suggestions on `Enter`. default: `false` - - `showGoalNames`: show goal names in Lean infoview box. default: `true` + - `compress`: compress code in URL. default: `true` - `mobile`: display code editor and infoview in narrow, vertically stacked, mobile-friendly mode. default: not set, i.e. inferred + - `showGoalNames`: show goal names in Lean infoview box. default: `true` + - `showExpectedType`: expected type in Lean infoview opened by default. default: `false` - `wordWrap`: wrap code in editor box. default: `true` - Non-boolean settings: - `abbreviationCharacter`: lead character for unicode abbreviations. values: a character. default: `\` From b8abef1a97b53e53a3623d56c6670fb98d09d86a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 04:25:33 +0100 Subject: [PATCH 3/5] lint --- tsconfig.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tsconfig.json b/tsconfig.json index e84daf92..fe2ba757 100644 --- a/tsconfig.json +++ b/tsconfig.json @@ -26,4 +26,4 @@ }, "include": ["client/src"], "exclude": ["server", "node_modules"] -} \ No newline at end of file +} From b76cbf95fe492da171d7280c3fe53c953277b684 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 04:26:42 +0100 Subject: [PATCH 4/5] undo --- .eslintrc.cjs | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/.eslintrc.cjs b/.eslintrc.cjs index 81b15e1a..d6c95379 100644 --- a/.eslintrc.cjs +++ b/.eslintrc.cjs @@ -9,5 +9,10 @@ module.exports = { ignorePatterns: ['dist', '.eslintrc.cjs'], parser: '@typescript-eslint/parser', plugins: ['react-refresh'], - rules: {}, + rules: { + 'react-refresh/only-export-components': [ + 'warn', + { allowConstantExport: true }, + ], + }, } From 4787819deceb5fb82dcf60a48740e1e5619755e7 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 28 Dec 2025 04:48:24 +0100 Subject: [PATCH 5/5] cleanup and fixes --- client/src/App.tsx | 18 +---- client/src/Navigation.tsx | 6 +- client/src/settings/SettingsPopup.tsx | 112 ++++++++++---------------- client/src/utils/shallowEqual.ts | 5 ++ 4 files changed, 55 insertions(+), 86 deletions(-) create mode 100644 client/src/utils/shallowEqual.ts diff --git a/client/src/App.tsx b/client/src/App.tsx index 32b93bda..b12da7c7 100644 --- a/client/src/App.tsx +++ b/client/src/App.tsx @@ -7,23 +7,17 @@ import LZString from 'lz-string' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' import { faCode } from '@fortawesome/free-solid-svg-icons' import * as path from 'path' - -// Local imports +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 { Entries } from './utils/Entries' import { save } from './utils/SaveToFile' import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing' -import { useWindowDimensions } from './utils/WindowWidth' - -// CSS import './css/App.css' import './css/Editor.css' -import { mobileAtom, settingsAtom, settingsUrlAtom } from './settings/settings-atoms' -import { useAtom } from 'jotai/react' -import { screenWidthAtom } from './store/window-atoms' -import { locationAtom } from './store/location-atoms' + /** Returns true if the browser wants dark mode */ function isBrowserDefaultDark() { @@ -65,10 +59,6 @@ function App() { setCode(code) } - useEffect(() => { - console.debug("location:",searchParams) - }, [searchParams]) - // Read the URL arguments useEffect(() => { // Parse args diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx index e6c8445e..655c306c 100644 --- a/client/src/Navigation.tsx +++ b/client/src/Navigation.tsx @@ -1,4 +1,4 @@ -import { ChangeEvent, Dispatch, FC, JSX, MouseEventHandler, ReactNode, SetStateAction, useContext, useState } from 'react' +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' @@ -15,9 +15,9 @@ import './css/Modal.css' import './css/Navigation.css' import { save } from './utils/SaveToFile' import { lookupUrl } from './utils/UrlParsing' -import { mobileAtom, settingsAtom } from './settings/settings-atoms' +import { mobileAtom } from './settings/settings-atoms' import { useAtom } from 'jotai' -import SettingsPopup from './settings/SettingsPopup' +import { SettingsPopup } from './settings/SettingsPopup' /** A button to appear in the hamburger menu or to navigation bar. */ export const NavButton: FC<{ diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx index 988a53a6..3344315e 100644 --- a/client/src/settings/SettingsPopup.tsx +++ b/client/src/settings/SettingsPopup.tsx @@ -1,69 +1,28 @@ -import { Dispatch, FC, SetStateAction, createContext, useContext, useState } from 'react' -import Switch from '@mui/material/Switch'; -import { Popup } from '../Navigation'; +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 { applySettingsAtom, settingsAtom } from './settings-atoms'; -import { useAtom } from 'jotai/react'; -import Slider from '@mui/material/Slider'; -import Box from '@mui/material/Box'; +import { shallowEqualSubset } from '../utils/shallowEqual' +import { inputAdornmentClasses } from '@mui/material/InputAdornment' -// /** The context holding the preferences */ -// export const PreferencesContext = createContext<{ -// preferences: Settings, -// setPreferences: Dispatch> -// }>({ -// preferences: defaultSettings, -// setPreferences: () => {}, -// }) - -// /** Save preferences to local storage whenever there are modifications */ -// function savePreferences(preferences: Settings) { -// console.debug("Preferences: Saving.") -// if (preferences.saveInLocalStore) { -// for (const [key, value] of Object.entries(preferences)) { -// if (typeof value === 'string') { -// window.localStorage.setItem(key, value) -// } else if (typeof value === 'boolean') { -// // turn boolean values into string -// window.localStorage.setItem(key, value ? 'true' : 'false') -// } else { -// // other values aren't implemented yet. -// console.error(`Preferences contain a value of unsupported type: ${typeof value}`) -// } -// } -// } else { -// for (const key in preferences) { -// window.localStorage.removeItem(key) -// } -// } -// } - -const marks: {value: number, label: string, key: MobileValues}[] = [ - { - value: 0, - label: 'Mobile', - key: true - }, - { - value: 1, - label: 'Auto', - key: "auto" - }, - { - value: 2, - label: 'Desktop', - key: false - }, - ]; - -const SettingsPopup: FC<{ +export function SettingsPopup({ + open, + handleClose, + closeNav, + project, + setProject +}: { open: boolean handleClose: () => void closeNav: () => void project: string - setProject: Dispatch> -}> = ({open, handleClose, closeNav, project, setProject}) => { + setProject: (project: string) => void +}) { const [settings, setSettings] = useAtom(settingsAtom) const [, applySettings] = useAtom(applySettingsAtom) const [newSettings, setNewSettings] = useState(settings) @@ -143,15 +102,15 @@ const SettingsPopup: FC<{ Layout: item.key === newSettings.mobile)?.value ?? 1} + value={mobileSliderMarks.find(item => item.key === newSettings.mobile)?.value ?? 1} step={1} - marks={marks} + marks={mobileSliderMarks} max={2} sx={{ '& .MuiSlider-track': { display: 'none', }, }} onChange={(_, val) => { - updateSetting("mobile", marks[val].key) + updateSetting("mobile", mobileSliderMarks[val].key) }} /> @@ -161,7 +120,10 @@ const SettingsPopup: FC<{ checked={newSettings.compress} />

- +

+ {updateSetting("inUrl", !newSettings.inUrl)}} checked={newSettings.inUrl} /> + +

Save

Editor settings and User settings are not preserved unless you opt-in to save them.

@@ -169,11 +131,7 @@ const SettingsPopup: FC<{

- {updateSetting("inUrl", !newSettings.inUrl)}} checked={newSettings.inUrl} /> - -

-

- {newSettings != defaultSettings && + {!shallowEqualSubset(defaultSettings, newSettings) && } } -export default SettingsPopup +const mobileSliderMarks: {value: number, label: string, key: MobileValues}[] = [ + { + value: 0, + label: 'Mobile', + key: true + }, + { + value: 1, + label: 'Auto', + key: "auto" + }, + { + value: 2, + label: 'Desktop', + key: false + }, +] diff --git a/client/src/utils/shallowEqual.ts b/client/src/utils/shallowEqual.ts new file mode 100644 index 00000000..19362d76 --- /dev/null +++ b/client/src/utils/shallowEqual.ts @@ -0,0 +1,5 @@ +/** Every key of `A` is in `B` and they have the same value. This is not syymmetric */ +export function shallowEqualSubset>(A: T, B: T): boolean { + const keysA = Object.keys(A) + return keysA.every(key => A[key] === B[key]) +} \ No newline at end of file