From 55f1fbf5ee245d29c9cdf1d7473d61ff01db15f3 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 9 Jun 2026 17:33:55 -0400 Subject: [PATCH 1/2] feat: more-standard settings for hiding the navigation bar --- client/src/NavBar.tsx | 223 +++++++++++++------------- client/src/context/NavBarContext.tsx | 47 ------ client/src/index.tsx | 10 +- client/src/navigation/Navigation.tsx | 20 ++- client/src/settings/SettingsPopup.tsx | 19 ++- client/src/settings/settings-atoms.ts | 58 ++++++- 6 files changed, 200 insertions(+), 177 deletions(-) delete mode 100644 client/src/context/NavBarContext.tsx diff --git a/client/src/NavBar.tsx b/client/src/NavBar.tsx index 5ca83991..0d88aa33 100644 --- a/client/src/NavBar.tsx +++ b/client/src/NavBar.tsx @@ -1,52 +1,51 @@ -import React, { useState } from "react"; -import "./css/Nav.css"; +import './css/Nav.css' -import GitHubIcon from "./assets/github.svg?react" -import MathLibLogo from "./assets/mathlib_initiative_logo.svg?react" -import { useNavBar } from "./context/NavBarContext"; +import { useAtomValue } from 'jotai' +import React, { useState } from 'react' + +import GitHubIcon from './assets/github.svg?react' +import MathLibLogo from './assets/mathlib_initiative_logo.svg?react' +import { navBarAtom } from './settings/settings-atoms' export interface NavItem { - title: React.ReactNode; - url?: string; - active?: boolean; - alt?: string; - classes?: string; - blank?: boolean; + title: React.ReactNode + url?: string + active?: boolean + alt?: string + classes?: string + blank?: boolean } const NavItemComponent: React.FC<{ item: NavItem }> = ({ item }) => { - const classes = item.classes ? ` ${item.classes}` : ""; + const classes = item.classes ? ` ${item.classes}` : '' return ( -
  • +
  • {item.url ? ( {item.title} ) : ( - )}
    • - ); -}; + ) +} interface NavBarProps { - logo: React.FC, - leftItems: NavItem[]; - rightItems: NavItem[]; - menuItems: NavItem[]; - externalLinks: NavItem[]; + logo: React.FC + leftItems: NavItem[] + rightItems: NavItem[] + menuItems: NavItem[] + externalLinks: NavItem[] classname: string } @@ -56,10 +55,10 @@ export const NavBar: React.FC = ({ rightItems, menuItems, externalLinks, - classname + classname, }) => { - const [isNavOpen, setIsNavOpen] = useState(false); - const [isFroOpen, setIsFroOpen] = useState(false); + const [isNavOpen, setIsNavOpen] = useState(false) + const [isFroOpen, setIsFroOpen] = useState(false) return (
    @@ -136,63 +135,63 @@ export const NavBar: React.FC = ({
    - ); -}; + ) +} -const LeanLogo: React.FC = () => - - - - - +const LeanLogo: React.FC = () => ( + + + + + +) const NavBarLean: React.FC = () => { const outItems: NavItem[] = [ - { title: "Playground", url: "https://live.lean-lang.org/", blank: true, active: true }, + { title: 'Playground', url: 'https://live.lean-lang.org/', blank: true, active: true }, { - title: "Reservoir", - url: "https://reservoir.lean-lang.org/", + title: 'Reservoir', + url: 'https://reservoir.lean-lang.org/', blank: true, }, - ]; + ] const rightItems: NavItem[] = [ { - title: , - alt: "Github", - url: "https://github.com/leanprover/lean4", + title: , + alt: 'Github', + url: 'https://github.com/leanprover/lean4', blank: true, }, - ]; + ] const leftItems: NavItem[] = [ - { title: "Install", url: "https://lean-lang.org/install" }, - { title: "Learn", url: "https://lean-lang.org/learn" }, - { title: "Community", url: "https://lean-lang.org/community" }, - { title: "Use Cases", url: "https://lean-lang.org/use-cases" }, - { title: "FRO", url: "https://lean-lang.org/fro" }, - ]; + { title: 'Install', url: 'https://lean-lang.org/install' }, + { title: 'Learn', url: 'https://lean-lang.org/learn' }, + { title: 'Community', url: 'https://lean-lang.org/community' }, + { title: 'Use Cases', url: 'https://lean-lang.org/use-cases' }, + { title: 'FRO', url: 'https://lean-lang.org/fro' }, + ] const menuItems = [ - { title: "Home", url: "https://lean-lang.org/fro" }, - { title: "About", url: "https://lean-lang.org/fro/about" }, - { title: "Team", url: "https://lean-lang.org/fro/team" }, - { title: "Roadmap", url: "https://lean-lang.org/fro/roadmap" }, - { title: "Contact", url: "https://lean-lang.org/fro/contact" }, - - ]; + { title: 'Home', url: 'https://lean-lang.org/fro' }, + { title: 'About', url: 'https://lean-lang.org/fro/about' }, + { title: 'Team', url: 'https://lean-lang.org/fro/team' }, + { title: 'Roadmap', url: 'https://lean-lang.org/fro/roadmap' }, + { title: 'Contact', url: 'https://lean-lang.org/fro/contact' }, + ] return ( { externalLinks={outItems} classname="lean" /> - ); -}; - -const MathLibIniciativeLogo = () => - + ) +} + +const MathLibIniciativeLogo = () => const NavBarMathLib: React.FC = () => { const outItems: NavItem[] = [ - { title: "Lean", url: "https://lean-lang.org/", blank: true }, - { title: "Mathlib Community", url: "https://leanprover-community.github.io/", blank: true }, - { title: "Playground", url: "https://live.lean-lang.org/?from=lean", blank: true, active: true }, - { title: "Reservoir", url: "https://reservoir.lean-lang.org/", blank: true }, - ]; + { title: 'Lean', url: 'https://lean-lang.org/', blank: true }, + { title: 'Mathlib Community', url: 'https://leanprover-community.github.io/', blank: true }, + { + title: 'Playground', + url: 'https://live.lean-lang.org/?from=lean', + blank: true, + active: true, + }, + { title: 'Reservoir', url: 'https://reservoir.lean-lang.org/', blank: true }, + ] const rightItems: NavItem[] = [ { - title: , - alt: "Github", - url: "https://github.com/leanprover/lean4", + title: , + alt: 'Github', + url: 'https://github.com/leanprover/lean4', blank: true, - } - ]; + }, + ] const leftItems: NavItem[] = [ - { title: "About", url: "https://mathlib-initiative.org/about" }, - { title: "Roadmap", url: "https://mathlib-initiative.org/roadmap" }, - { title: "Team", url: "https://mathlib-initiative.org/team" }, - { title: "Careers", url: "https://mathlib-initiative.org/careers" }, - { title: "Support Us", url: "https://mathlib-initiative.org/support" }, - { title: "Contact", url: "https://mathlib-initiative.org/contact" }, - ]; + { title: 'About', url: 'https://mathlib-initiative.org/about' }, + { title: 'Roadmap', url: 'https://mathlib-initiative.org/roadmap' }, + { title: 'Team', url: 'https://mathlib-initiative.org/team' }, + { title: 'Careers', url: 'https://mathlib-initiative.org/careers' }, + { title: 'Support Us', url: 'https://mathlib-initiative.org/support' }, + { title: 'Contact', url: 'https://mathlib-initiative.org/contact' }, + ] const menuItems = [ - { title: "Home", url: "https://lean-lang.org/fro" }, - { title: "About", url: "https://lean-lang.org/fro/about" }, - { title: "Team", url: "https://lean-lang.org/fro/team" }, - { title: "Roadmap", url: "https://lean-lang.org/fro/roadmap" }, - { title: "Contact", url: "https://lean-lang.org/fro/contact" }, - - ]; + { title: 'Home', url: 'https://lean-lang.org/fro' }, + { title: 'About', url: 'https://lean-lang.org/fro/about' }, + { title: 'Team', url: 'https://lean-lang.org/fro/team' }, + { title: 'Roadmap', url: 'https://lean-lang.org/fro/roadmap' }, + { title: 'Contact', url: 'https://lean-lang.org/fro/contact' }, + ] return ( { externalLinks={outItems} classname="mathlib" /> - ); -}; - + ) +} const NavBarComp: React.FC = () => { - let navBar = useNavBar() - - return (!navBar.hideNavBar && <> - {navBar.requiresNavBar === 1 && } - {navBar.requiresNavBar === 2 && } - ) - + const navBar = useAtomValue(navBarAtom) + return ( + <> + {navBar === 'mathlib' && } + {navBar === 'lean' && } + + ) } -export {NavBarLean, NavBarMathLib, NavBarComp}; \ No newline at end of file +export { NavBarComp, NavBarLean, NavBarMathLib } diff --git a/client/src/context/NavBarContext.tsx b/client/src/context/NavBarContext.tsx deleted file mode 100644 index b9514aae..00000000 --- a/client/src/context/NavBarContext.tsx +++ /dev/null @@ -1,47 +0,0 @@ -import React, { createContext, useContext, useEffect, useState } from "react"; - -type NavBarContextType = { - requiresNavBar: number; - setRequiresNavBar: React.Dispatch>; - hideNavBar: boolean; - setHideNavBar: React.Dispatch>; -}; - -const NavBarContext = createContext(undefined); - -export const NavBarProvider: React.FC<{ children: React.ReactNode }> = ({ children }) => { - const [requiresNavBar, setRequiresNavBar] = useState(() => { - const params = new URLSearchParams(window.location.search); - const fromParam = params.get("from"); - if (fromParam === "mathlib") return 1; - else if (fromParam === "lean") return 2; - return 0; - }); - - const [hideNavBar, setHideNavBar] = useState(() => { - const params = new URLSearchParams(window.location.search); - const hideParam = params.get("hide"); - if (hideParam) return hideParam === "true"; - - const stored = localStorage.getItem("hideNavBar"); - return stored ? stored === "true" : false; - }); - - useEffect(() => { - localStorage.setItem("hideNavBar", hideNavBar.toString()); - }, [hideNavBar]); - - return ( - - {children} - - ); -}; - -export const useNavBar = () => { - const ctx = useContext(NavBarContext); - if (!ctx) throw new Error("useNavBar must be used inside a NavBarProvider"); - return ctx; -}; diff --git a/client/src/index.tsx b/client/src/index.tsx index 1b563571..5554f79b 100644 --- a/client/src/index.tsx +++ b/client/src/index.tsx @@ -3,16 +3,12 @@ import './css/index.css' import { StrictMode } from 'react' import ReactDOM from 'react-dom/client' -import { NavBarProvider } from './context/NavBarContext.tsx' -import { NavBarLean, NavBar, NavItem, NavBarMathLib, NavBarComp } from './NavBar' - import App from './App.tsx' +import { NavBarComp } from './NavBar.tsx' ReactDOM.createRoot(document.getElementById('root')!).render( - - - - + + , ) diff --git a/client/src/navigation/Navigation.tsx b/client/src/navigation/Navigation.tsx index f6100f0a..2f7cde95 100644 --- a/client/src/navigation/Navigation.tsx +++ b/client/src/navigation/Navigation.tsx @@ -1,7 +1,7 @@ import '../css/Modal.css' import '../css/Navigation.css' -import { faArrowRotateRight, faCode, faInfoCircle, faEye } from '@fortawesome/free-solid-svg-icons' +import { faArrowRotateRight, faCode, faEye, faInfoCircle } from '@fortawesome/free-solid-svg-icons' import { faArrowUpRightFromSquare, faBars, @@ -15,7 +15,7 @@ import { faXmark, } from '@fortawesome/free-solid-svg-icons' import { FontAwesomeIcon } from '@fortawesome/react-fontawesome' -import { useAtom } from 'jotai' +import { useAtom, useAtomValue } from 'jotai' import { ChangeEvent, Dispatch, SetStateAction, useState } from 'react' import { lean4webConfig } from '../../config' @@ -26,7 +26,7 @@ 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 { localOnlySettingAtom, mobileAtom, navBarRequestedAtom } from '../settings/settings-atoms' import { SettingsPopup } from '../settings/SettingsPopup' import { setImportUrlAndProjectAtom } from '../store/import-atoms' import { currentProjectAtom, projectsAtom, visibleProjectsAtom } from '../store/project-atoms' @@ -34,8 +34,6 @@ import { save } from '../utils/SaveToFile' import { Dropdown } from './Dropdown' import { NavButton } from './NavButton' -import { useNavBar } from '../context/NavBarContext' - /** The menu items either appearing inside the dropdown or outside */ function FlexibleMenu({ isInDropdown = false, @@ -177,8 +175,8 @@ export function Menu({ const [mobile] = useAtom(mobileAtom) const hasImpressum = lean4webConfig.impressum || lean4webConfig.contactDetails - - let navbar = useNavBar() + const navBarRequested = useAtomValue(navBarRequestedAtom); + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingAtom) return (
    @@ -251,7 +249,13 @@ export function Menu({ }} /> setToolsOpen(true)} /> - { navbar.requiresNavBar != 0 && navbar.setHideNavBar(!navbar.hideNavBar)} />} + {navBarRequested !== null && ( + setLocalOnlySettings('hideNavbar', !localOnlySettings.hideNavbar)} + /> + )} (settings) + const [localOnlySettings, setLocalOnlySettings] = useAtom(localOnlySettingAtom) function updateSetting(key: K, value: Settings[K]) { setNewSettings((prev) => ({ ...prev, [key]: value })) @@ -52,7 +53,6 @@ export function SettingsPopup({ )}

    */} -

    Editor settings

    -

    User settings

    @@ -198,6 +197,20 @@ export function SettingsPopup({ onClick={() => applySettings(newSettings)} />

    +

    Local Settings

    +

    + These settings are always preserved in the browser's local storage. +

    +

    + { + setLocalOnlySettings('hideNavbar', !localOnlySettings.hideNavbar) + }} + checked={!!localOnlySettings.hideNavbar} + /> + +

    ) diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index a777f43a..5c77ddd4 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -1,4 +1,4 @@ -import { atomWithStorage, selectAtom } from 'jotai/utils' +import { atomWithStorage, createJSONStorage, selectAtom } from 'jotai/utils' import { atom } from 'jotai/vanilla' import { locationAtom } from '../store/location-atoms' @@ -13,6 +13,62 @@ const settingsStoreAtom = atomWithStorage('lean4web:setting getOnInit: true, }) +/** "Local Only" settings: always stored on localstorage, never in the URL, always in local storage */ +interface PartialLocalOnlyUserSettings { + /** Hide the navigation bar that otherwise appears when `?from=lean` or `?from=mathlib` is set. */ + hideNavbar?: boolean +} + +const localOnlyStorage = createJSONStorage(() => localStorage) + +/** Delete local storage if all items become falsy */ +const prunedLocalOnlyStorage: typeof localOnlyStorage = { + ...localOnlyStorage, + setItem(key, value) { + if (Object.keys(value).length === 0) { + localOnlyStorage.removeItem(key) + } else { + localOnlyStorage.setItem(key, value) + } + }, +} + +const fullLocalOnlySettingsAtom = atomWithStorage( + 'lean4web:local-settings', + localStorage.getItem('hideNavBar') === 'true' ? { hideNavbar: true } : {}, + prunedLocalOnlyStorage, + { getOnInit: true }, +) + +/** Local-only settings are always stored in local storage, never in the URL */ +export const localOnlySettingAtom = atom( + (get) => get(fullLocalOnlySettingsAtom), + (get, set, key: keyof PartialLocalOnlyUserSettings, value: boolean) => { + const next = { ...get(fullLocalOnlySettingsAtom) } + if (!value) { + delete next[key] + } else { + next[key] = true + } + set(fullLocalOnlySettingsAtom, next) + }, +) + +/** Static: do the URL's search parameters indicate that we should show a navigation header? */ +export const navBarRequestedAtom = atom(() => { + const params = new URLSearchParams(window.location.search) + const fromParam = params.get('from') + if (fromParam === 'mathlib') return 'mathlib' + if (fromParam === 'lean') return 'lean' + return null +}) + +/** Which navigation header will be shown */ +export const navBarAtom = atom((get) => { + if (get(localOnlySettingAtom).hideNavbar) return null + return get(navBarRequestedAtom) +}) + /** The settings which are set in the searchParams of the opened URL */ const settingsUrlAtom = atom( (get) => { From 100237eca086260e607caf030fb8c38eaa10a204 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 9 Jun 2026 18:16:42 -0400 Subject: [PATCH 2/2] migration --- client/src/settings/settings-atoms.ts | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts index 5c77ddd4..b4644989 100644 --- a/client/src/settings/settings-atoms.ts +++ b/client/src/settings/settings-atoms.ts @@ -19,6 +19,14 @@ interface PartialLocalOnlyUserSettings { hideNavbar?: boolean } +// Migrate legacy `hideNavBar` option to new setting (added June 2026, delete after October 2026) +if (localStorage.getItem('hideNavBar')) { + if (localStorage.getItem('hideNavBar') === "true") { + localStorage.setItem("lean4web:local-settings", '{"hideNavbar":true}') + } + localStorage.removeItem('hideNavBar') +} + const localOnlyStorage = createJSONStorage(() => localStorage) /** Delete local storage if all items become falsy */ @@ -35,7 +43,7 @@ const prunedLocalOnlyStorage: typeof localOnlyStorage = { const fullLocalOnlySettingsAtom = atomWithStorage( 'lean4web:local-settings', - localStorage.getItem('hideNavBar') === 'true' ? { hideNavbar: true } : {}, + {}, prunedLocalOnlyStorage, { getOnInit: true }, )