From 73911b76dc74b13477aaf753bdb83ad2e380aa38 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sat, 27 Dec 2025 23:25:08 +0100
Subject: [PATCH 1/2] refactor/settings-in-jotai

---
 client/src/App.tsx                            | 125 ++++--------
 client/src/Navigation.tsx                     |  12 +-
 client/src/Popups/LoadUrl.tsx                 |   2 +-
 client/src/Popups/LoadZulip.tsx               |   2 +-
 client/src/Popups/Settings.tsx                | 142 -------------
 client/src/css/App.css                        |   5 +
 client/src/css/Modal.css                      |  10 +-
 client/src/settings/SettingsPopup.tsx         | 191 ++++++++++++++++++
 client/src/settings/settings-atoms.ts         |  48 +++++
 .../settings-types.ts}                        |  33 ++-
 client/src/store/window-atoms.ts              |   9 +
 cypress/e2e/settings.cy.ts                    |  42 ++++
 cypress/e2e/spec.cy.ts                        |  36 ----
 doc/Usage.md                                  |   2 +-
 package-lock.json                             |  75 +++++--
 package.json                                  |   2 +
 16 files changed, 430 insertions(+), 306 deletions(-)
 delete mode 100644 client/src/Popups/Settings.tsx
 create mode 100644 client/src/settings/SettingsPopup.tsx
 create mode 100644 client/src/settings/settings-atoms.ts
 rename client/src/{config/settings.ts => settings/settings-types.ts} (69%)
 create mode 100644 client/src/store/window-atoms.ts
 create mode 100644 cypress/e2e/settings.cy.ts

diff --git a/client/src/App.tsx b/client/src/App.tsx
index 83babe88..91617e01 100644
--- a/client/src/App.tsx
+++ b/client/src/App.tsx
@@ -10,9 +10,8 @@ import * as path from 'path'
 
 // Local imports
 import LeanLogo from './assets/logo.svg'
-import defaultSettings, { IPreferencesContext, lightThemes, preferenceParams } from './config/settings'
+import { lightThemes } from './settings/settings-types'
 import { Menu } from './Navigation'
-import { PreferencesContext } from './Popups/Settings'
 import { Entries } from './utils/Entries'
 import { save } from './utils/SaveToFile'
 import { fixedEncodeURIComponent, formatArgs, lookupUrl, parseArgs } from './utils/UrlParsing'
@@ -21,6 +20,9 @@ import { useWindowDimensions } from './utils/WindowWidth'
 // CSS
 import './css/App.css'
 import './css/Editor.css'
+import { mobileAtom, settingsAtom } from './settings/settings-atoms'
+import { useAtom } from 'jotai/react'
+import { screenWidthAtom } from './store/window-atoms'
 
 /** Returns true if the browser wants dark mode */
 function isBrowserDefaultDark() {
@@ -33,8 +35,9 @@ function App() {
   const [dragging, setDragging] = useState<boolean | null>(false)
   const [editor, setEditor] = useState<monaco.editor.IStandaloneCodeEditor>()
   const [leanMonaco, setLeanMonaco] = useState<LeanMonaco>()
-  const [loaded, setLoaded] = useState<boolean>(false)
-  const [preferences, setPreferences] = useState<IPreferencesContext>(defaultSettings)
+  const [settings] = useAtom(settingsAtom)
+  const [mobile] = useAtom(mobileAtom)
+  const [, setScreenWidth] = useAtom(screenWidthAtom)
   const { width } = useWindowDimensions()
 
   // Lean4monaco options
@@ -83,67 +86,13 @@ function App() {
     setProject(project)
   }, [])
 
-  // Load preferences from store in the beginning
+  // save the screen width in jotai
   useEffect(() => {
-    // only load them once
-    if (loaded) { return }
-    console.debug('[Lean4web] Loading preferences')
-
-    let saveInLocalStore = false;
-    let newPreferences: { [K in keyof IPreferencesContext]: IPreferencesContext[K] } = { ...preferences }
-    for (const [key, value] of (Object.entries(preferences) as Entries<IPreferencesContext>)) {
-      // prefer URL params over stored
-      const searchParams = new URLSearchParams(window.location.search);
-      let storedValue = (
-        preferenceParams.includes(key) &&  // only for keys we explictly check for
-        searchParams.has(key) && searchParams.get(key))
-        ?? window.localStorage.getItem(key)
-      if (storedValue) {
-        saveInLocalStore = window.localStorage.getItem(key) === storedValue
-        console.debug(`[Lean4web] Found value for ${key}: ${storedValue}`)
-        if (typeof value === 'string') {
-          if (key == 'theme') {
-            const theme = storedValue.toLowerCase().includes('dark') ? "Visual Studio Dark" : "Visual Studio Light"
-            newPreferences[key] = theme
-          }
-          else {
-            newPreferences[key] = storedValue
-          }
-        } else if (typeof value === 'boolean') {
-          newPreferences[key] = (storedValue === "true")
-        } else {
-          // other values aren't implemented yet.
-          console.error(`[Lean4web] Preferences (key: ${key}) contain a value of unsupported type: ${typeof value}`)
-        }
-      } else {
-        // no stored preferences, set a default value
-        if (key == 'theme') {
-          if (isBrowserDefaultDark()) {
-            console.debug("[Lean4web] Preferences: Set dark theme.")
-            newPreferences['theme'] = 'Visual Studio Dark'
-          } else {
-            console.debug("[Lean4web] Preferences: Set light theme.")
-            newPreferences['theme'] = 'Visual Studio Light'
-          }
-        }
-      }
-    }
-    newPreferences['saveInLocalStore'] = saveInLocalStore
-    setPreferences(newPreferences)
-    setLoaded(true)
-  }, [])
-
-  // Use the window width to switch between mobile/desktop layout
-  useEffect(() => {
-    // Wait for preferences to be loaded
-    if (!loaded) { return }
+    const handleResize = () => setScreenWidth(window.innerWidth)
+    window.addEventListener('resize', handleResize)
+    return () => window.removeEventListener('resize', handleResize)
+  }, [setScreenWidth])
 
-    const _mobile = width < 800
-    const searchParams = new URLSearchParams(window.location.search);
-    if (!(searchParams.has("mobile") || preferences.saveInLocalStore) && _mobile !== preferences.mobile) {
-      setPreferences({ ...preferences, mobile: _mobile })
-    }
-  }, [width, loaded])
 
   // Update LeanMonaco options when preferences are loaded or change
   useEffect(() => {
@@ -162,29 +111,28 @@ function App() {
          * for the desired setting, select "Copy Setting as JSON" from the "More Actions"
          * menu next to the selected setting, and paste the copied string here.
          */
-        "workbench.colorTheme": preferences.theme,
+        "workbench.colorTheme": settings.theme,
         "editor.tabSize": 2,
         // "editor.rulers": [100],
         "editor.lightbulb.enabled": "on",
-        "editor.wordWrap": preferences.wordWrap ? "on" : "off",
+        "editor.wordWrap": settings.wordWrap ? "on" : "off",
         "editor.wrappingStrategy": "advanced",
         "editor.semanticHighlighting.enabled": true,
-        "editor.acceptSuggestionOnEnter": preferences.acceptSuggestionOnEnter ? "on" : "off",
+        "editor.acceptSuggestionOnEnter": settings.acceptSuggestionOnEnter ? "on" : "off",
         "lean4.input.eagerReplacementEnabled": true,
-        "lean4.infoview.showGoalNames": preferences.showGoalNames,
+        "lean4.infoview.showGoalNames": settings.showGoalNames,
         "lean4.infoview.emphasizeFirstGoal": true,
         "lean4.infoview.showExpectedType": false,
         "lean4.infoview.showTooltipOnHover": false,
-        "lean4.input.leader": preferences.abbreviationCharacter
+        "lean4.input.leader": settings.abbreviationCharacter
       }
     }
     setOptions(_options)
-  }, [editorRef, project, preferences])
+  }, [editorRef, project, settings])
 
   // Setting up the editor and infoview
   useEffect(() => {
-    // Wait for preferences to be loaded
-    if (!loaded) { return }
+    // if (project === undefined) return
     console.debug('[Lean4web] Restarting editor')
     var _leanMonaco = new LeanMonaco()
     var leanMonacoEditor = new LeanMonacoEditor()
@@ -192,7 +140,7 @@ function App() {
     _leanMonaco.setInfoviewElement(infoviewRef.current!)
     ;(async () => {
         await _leanMonaco.start(options)
-        await leanMonacoEditor.start(editorRef.current!, path.join(project, `${project}.lean`), code)
+        await leanMonacoEditor.start(editorRef.current!, path.join(project, `${project}.lean`), code ?? '')
 
         setEditor(leanMonacoEditor.editor)
         setLeanMonaco(_leanMonaco)
@@ -201,7 +149,7 @@ function App() {
         // Monaco does not support clipboard pasting as all browsers block it
         // due to security reasons. Therefore we use a codeMirror editor overlay
         // which features good mobile support (but no Lean support yet)
-        if (preferences.mobile) {
+        if (mobile) {
           leanMonacoEditor.editor?.addAction({
             id: "myPaste",
             label: "Paste: open 'Plain Editor' for editing on mobile",
@@ -274,7 +222,7 @@ function App() {
       leanMonacoEditor.dispose()
       _leanMonaco.dispose()
     }
-  }, [loaded, project, preferences, options, infoviewRef, editorRef])
+  }, [project, settings, options, infoviewRef, editorRef])
 
   // Load content from source URL.
   // Once the editor is loaded, this reads the content of any provided `url=` in the URL and
@@ -330,7 +278,7 @@ function App() {
         code: null,
         codez: null
       }
-    } else if (preferences.compress) {
+    } 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(/=*$/, '')
@@ -402,7 +350,7 @@ function App() {
     }
   }, [handleKeyDown, handleKeyUp])
 
-  return <PreferencesContext.Provider value={{preferences, setPreferences}}>
+  return (
     <div className="app monaco-editor">
       <nav>
         <LeanLogo />
@@ -426,20 +374,20 @@ function App() {
         }}
         gutterStyle={(_dimension, gutterSize, _index) => {
           return {
-            'width': preferences.mobile ? '100%' : `${gutterSize}px`,
-            'height': preferences.mobile ? `${gutterSize}px` : '100%',
-            'cursor': preferences.mobile ? 'row-resize' : 'col-resize',
-            'margin-left': preferences.mobile ? 0 : `-${gutterSize}px`,
-            'margin-top': preferences.mobile ? `-${gutterSize}px` : 0,
+            'width': mobile ? '100%' : `${gutterSize}px`,
+            'height': mobile ? `${gutterSize}px` : '100%',
+            'cursor': mobile ? 'row-resize' : 'col-resize',
+            'margin-left': mobile ? 0 : `-${gutterSize}px`,
+            'margin-top': mobile ? `-${gutterSize}px` : 0,
             'z-index': 0,
           }}}
         gutterSize={5}
         onDragStart={() => setDragging(true)} onDragEnd={() => setDragging(false)}
-        sizes={preferences.mobile ? [50, 50] : [70, 30]}
-        direction={preferences.mobile ? "vertical" : "horizontal"}
-        style={{flexDirection: preferences.mobile ? "column" : "row"}}>
+        sizes={mobile ? [50, 50] : [70, 30]}
+        direction={mobile ? "vertical" : "horizontal"}
+        style={{flexDirection: mobile ? "column" : "row"}}>
         <div className='codeview-wrapper'
-          style={preferences.mobile ? {width : '100%'} : {height: '100%'}} >
+          style={mobile ? {width : '100%'} : {height: '100%'}} >
           { codeMirror &&
             <CodeMirror
               className="codeview plain"
@@ -447,13 +395,13 @@ function App() {
               extensions={[EditorView.lineWrapping]}
               height='100%'
               maxHeight='100%'
-              theme={lightThemes.includes(preferences.theme) ? 'light' : 'dark'}
+              theme={lightThemes.includes(settings.theme) ? 'light' : 'dark'}
               onChange={setContent} />
           }
           <div ref={editorRef} className={`codeview${codeMirror ? ' hidden' : ''}`} />
         </div>
         <div ref={infoviewRef} className="vscode-light infoview"
-          style={preferences.mobile ? {width : '100%'} : {height: '100%'}} >
+          style={mobile ? {width : '100%'} : {height: '100%'}} >
             <p className={`editor-support-warning${codeMirror ? '' : ' hidden'}`} >
               You are in the plain text editor<br /><br />
               Go back to the Monaco Editor (click <FontAwesomeIcon icon={faCode}/>)
@@ -462,8 +410,7 @@ function App() {
         </div>
       </Split>
     </div>
-  </PreferencesContext.Provider>
-
+  )
 }
 
 export default App
diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx
index 3bb2370d..e6c8445e 100644
--- a/client/src/Navigation.tsx
+++ b/client/src/Navigation.tsx
@@ -4,7 +4,6 @@ import { IconDefinition, faArrowRotateRight, faCode, faInfoCircle } from '@forta
 import ZulipIcon from './assets/zulip.svg'
 import { faArrowUpRightFromSquare, faDownload, faBars, faXmark, faShield, faHammer, faGear, faStar, faUpload, faCloudArrowUp } from '@fortawesome/free-solid-svg-icons'
 
-import SettingsPopup, { PreferencesContext } from './Popups/Settings'
 import PrivacyPopup from './Popups/PrivacyPolicy'
 import ImpressumPopup from './Popups/Impressum'
 import ToolsPopup from './Popups/Tools'
@@ -16,6 +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 { useAtom } from 'jotai'
+import SettingsPopup from './settings/SettingsPopup'
 
 /** A button to appear in the hamburger menu or to navigation bar. */
 export const NavButton: FC<{
@@ -154,7 +156,7 @@ export const Menu: FC <{
   const [toolsOpen, setToolsOpen] = useState(false)
   const [settingsOpen, setSettingsOpen] = useState(false)
 
-  const { preferences } = useContext(PreferencesContext)
+  const [mobile] = useAtom(mobileAtom)
 
   const loadFromUrl = (url: string, project:string|undefined=undefined) => {
     url = lookupUrl(url)
@@ -184,10 +186,10 @@ export const Menu: FC <{
         <option key={proj.folder} value={proj.folder}>{proj.name ?? proj.folder}</option>
       )}
     </select>
-    { preferences.mobile &&
+    { mobile &&
       <NavButton icon={faCode} text={codeMirror ? "Lean" : "Text"} onClick={() => {setCodeMirror(!codeMirror)}}/>
     }
-    { !preferences.mobile &&
+    { !mobile &&
       <FlexibleMenu isInDropdown={false}
         setOpenNav={setOpenNav}
         openExample={openExample}
@@ -200,7 +202,7 @@ export const Menu: FC <{
         setLoadZulipOpen={setLoadZulipOpen} />
     }
     <Dropdown open={openNav} setOpen={setOpenNav} icon={openNav ? faXmark : faBars} onClick={() => {setOpenExample(false); setOpenLoad(false)}}>
-      { preferences.mobile &&
+      { mobile &&
         <FlexibleMenu isInDropdown={true}
           setOpenNav={setOpenNav}
           openExample={openExample}
diff --git a/client/src/Popups/LoadUrl.tsx b/client/src/Popups/LoadUrl.tsx
index c96e27f0..0ac80283 100644
--- a/client/src/Popups/LoadUrl.tsx
+++ b/client/src/Popups/LoadUrl.tsx
@@ -28,7 +28,7 @@ const LoadUrlPopup: FC<{
     <h2>Load from URL</h2>
     {error ? <p className="form-error">{error}</p>: null}
     <form onSubmit={handleLoad}>
-      <input autoFocus type="text" placeholder="Paste URL here" ref={urlRef}/>
+      <input name="import URL" autoFocus type="text" placeholder="Paste URL here" ref={urlRef}/>
       <input type="submit" value="Load"/>
     </form>
   </Popup>
diff --git a/client/src/Popups/LoadZulip.tsx b/client/src/Popups/LoadZulip.tsx
index 841c064a..20eae0d9 100644
--- a/client/src/Popups/LoadZulip.tsx
+++ b/client/src/Popups/LoadZulip.tsx
@@ -42,7 +42,7 @@ const LoadZulipPopup: FC<{
     </p>
     {error ? <p className="form-error">{error}</p>: null}
     <form onSubmit={handleLoad}>
-    <textarea autoFocus placeholder="Paste Zulip message" ref={textInputRef}/>
+    <textarea name="Zulip message input" autoFocus placeholder="Paste Zulip message" ref={textInputRef}/>
     <input type="submit" value="Parse message"/>
     </form>
   </Popup>
diff --git a/client/src/Popups/Settings.tsx b/client/src/Popups/Settings.tsx
deleted file mode 100644
index cff1c886..00000000
--- a/client/src/Popups/Settings.tsx
+++ /dev/null
@@ -1,142 +0,0 @@
-import { Dispatch, FC, SetStateAction, createContext, useContext } from 'react'
-import Switch from '@mui/material/Switch';
-import lean4webConfig from '../config/config'
-import { Popup } from '../Navigation';
-import defaultSettings, { IPreferencesContext } from '../config/settings'
-
-/** The context holding the preferences */
-export const PreferencesContext = createContext<{
-  preferences: IPreferencesContext,
-  setPreferences: Dispatch<SetStateAction<IPreferencesContext>>
-}>({
-  preferences: defaultSettings,
-  setPreferences: () => {},
-})
-
-/** Save preferences to local storage whenever there are modifications */
-function savePreferences(preferences: IPreferencesContext) {
-  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 SettingsPopup: FC<{
-  open: boolean
-  handleClose: () => void
-  closeNav: () => void
-  project: string
-  setProject: Dispatch<SetStateAction<string>>
-}> = ({open, handleClose, closeNav, project, setProject}) => {
-  const { preferences, setPreferences } = useContext(PreferencesContext)
-
-  function modifyPreferences(key: keyof IPreferencesContext, value: any) {
-    let newPreferences: any = { ...preferences } // TODO: need `any` instead of `IPreferencesContext` here to satisfy ts
-    newPreferences[key] = value
-    setPreferences(newPreferences)
-  }
-
-  return <Popup open={open} handleClose={handleClose}>
-    <form onSubmit={(ev) => {ev.preventDefault(); handleClose(); closeNav()}}>
-      <h2>Project settings</h2>
-      <p><i>These settings are stored in the URL as they change the project's setup</i></p>
-      <p>
-        <label htmlFor="leanVersion">Lean Version: </label>
-        <select
-            id="leanVersion"
-            name="leanVersion"
-            value={project}
-            onChange={(ev) => {
-              setProject(ev.target.value)
-              console.log(`set Lean project to: ${ev.target.value}`)
-              }} >
-          {lean4webConfig.projects.map(proj =>
-            <option key={proj.folder} value={proj.folder}>{proj.name ?? proj.folder}</option>
-          )}
-        </select>
-      </p>
-
-      <h2>Editor settings</h2>
-      <p>
-        <label htmlFor="abbreviationCharacter">Lead character to trigger unicode input mode</label>
-        <input id="abbreviationCharacter" type="text"
-          onChange={(ev) => {modifyPreferences("abbreviationCharacter", ev.target.value)}}
-          value={preferences.abbreviationCharacter} />
-      </p>
-      <p>
-        <Switch id="wordWrap" onChange={() => {modifyPreferences("wordWrap", !preferences.wordWrap)}}
-        checked={preferences.wordWrap} />
-        <label htmlFor="wordWrap">Wrap code</label>
-      </p>
-      <p>
-        <Switch id="acceptSuggestionOnEnter" onChange={() => {modifyPreferences("acceptSuggestionOnEnter", !preferences.acceptSuggestionOnEnter)}}
-        checked={preferences.acceptSuggestionOnEnter} />
-        <label htmlFor="acceptSuggestionOnEnter">Accept Suggestion on Enter</label>
-      </p>
-      <p>
-        <Switch id="showGoalNames" onChange={() => {modifyPreferences("showGoalNames", !preferences.showGoalNames)}}
-        checked={preferences.showGoalNames} />
-        <label htmlFor="showGoalNames">Show Goal Names</label>
-      </p>
-
-      <h2>User settings</h2>
-      <p>
-        <label htmlFor="theme">Theme: </label>
-        <select
-            id="theme"
-            name="theme"
-            value={preferences.theme}
-            onChange={(ev) => {modifyPreferences("theme", ev.target.value)}}
-            >
-          <option value="Visual Studio Light">visual studio light</option>
-          <option value="Visual Studio Dark">visual studio dark</option>
-          {/* <option value="Default Light+">light+</option> */}
-          {/* <option value="Default Dark+">dark+</option> */}
-          {/* <option value="Default Light Modern">light modern</option> */}
-          <option value="Default High Contrast">high contrast</option>
-          <option value="Cobalt">cobalt</option>
-
-        </select>
-      </p>
-      <p>
-        <Switch id="mobile" onChange={() => {
-          modifyPreferences("mobile", !preferences.mobile)
-          // ev.stopPropagation()
-        }} checked={preferences.mobile}
-        />
-        <label htmlFor="mobile">Mobile layout (vertical)</label>
-      </p>
-      <p>
-        <Switch id="compress" onChange={() => {modifyPreferences("compress", !preferences.compress)}}
-        checked={preferences.compress} />
-        <label htmlFor="compress">Compress code in URL</label>
-      </p>
-
-      <h2>Save</h2>
-      <p><i>Editor settings and User settings are not preserved unless you opt-in to save them.</i></p>
-      <p>
-        <Switch id="savingAllowed" onChange={() => {modifyPreferences("saveInLocalStore", !preferences.saveInLocalStore)}} checked={preferences.saveInLocalStore} />
-        <label htmlFor="savingAllowed">Save my settings (in the browser store)</label>
-      </p>
-      <p>
-        <input type="submit" value={preferences.saveInLocalStore?"Save":"OK"} onClick={() => {savePreferences(preferences)}}/>
-      </p>
-    </form>
-  </Popup>
-}
-
-export default SettingsPopup
diff --git a/client/src/css/App.css b/client/src/css/App.css
index d6b5bb22..b5f98472 100644
--- a/client/src/css/App.css
+++ b/client/src/css/App.css
@@ -36,3 +36,8 @@
 .hidden {
   display: none !important;
 }
+
+:root {
+  --vscode-editor-background: #1e1e1e;
+  --vscode-editor-foreground: #d4d4d4;
+}
\ No newline at end of file
diff --git a/client/src/css/Modal.css b/client/src/css/Modal.css
index e12d7b4e..9a2c4ff6 100644
--- a/client/src/css/Modal.css
+++ b/client/src/css/Modal.css
@@ -32,6 +32,8 @@ input[type="file"] {
   transform: translate(-50%, -50%);
   min-width: 50%;
   max-width: 60ch;
+  max-height: 90%;
+  overflow-y: auto;
   background: var(--vscode-input-background);
   z-index: 3;
   padding: 2rem;
@@ -41,6 +43,10 @@ input[type="file"] {
   color: var(--vscode-input-foreground);
 }
 
+.modal .MuiSlider-markLabel {
+  color: var(--vscode-input-foreground);
+}
+
 @media only screen and (max-width: 800px) {
   .modal {
     min-width: 90%;
@@ -62,7 +68,7 @@ input[type="file"] {
   font-weight: bold;
 }
 
-.modal input[type="submit"], .modal .file-upload-button {
+.modal input[type="submit"], .modal button, .modal .file-upload-button {
   border: none;
   color: var(--vscode-button-foreground);
   background: var(--vscode-button-background);
@@ -71,7 +77,7 @@ input[type="file"] {
   border-radius: .2rem;
 }
 
-.modal input[type="submit"]{
+.modal input[type="submit"], .modal button {
   display: block;
   margin: 1rem auto;
 }
diff --git a/client/src/settings/SettingsPopup.tsx b/client/src/settings/SettingsPopup.tsx
new file mode 100644
index 00000000..1409f6ae
--- /dev/null
+++ b/client/src/settings/SettingsPopup.tsx
@@ -0,0 +1,191 @@
+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 { useAtom } from 'jotai/react';
+import FormControlLabel from '@mui/material/FormControlLabel';
+import Slider from '@mui/material/Slider';
+import Box from '@mui/material/Box';
+
+// /** The context holding the preferences */
+// export const PreferencesContext = createContext<{
+//   preferences: Settings,
+//   setPreferences: Dispatch<SetStateAction<Settings>>
+// }>({
+//   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<{
+  open: boolean
+  handleClose: () => void
+  closeNav: () => void
+  project: string
+  setProject: Dispatch<SetStateAction<string>>
+}> = ({open, handleClose, closeNav, project, setProject}) => {
+  const [hasSettingsSaved] = useAtom(hasSettingsSavedAtom)
+  const [settings, setSettings] = useAtom(settingsAtom)
+  const [, applyAndSaveStore] = useAtom(applyAndSaveSettingsAtom)
+  const [, applyAndClearStore] = useAtom(applySettingsAtom)
+  const [newSettings, setNewSettings] = useState<Settings>(settings)
+  const [allowSaveInStore, setAllowSaveInStore] = useState<boolean>(hasSettingsSaved)
+
+  function updateSetting<K extends keyof Settings>(key: K, value: Settings[K]) {
+    setNewSettings(prev => ({ ...prev, [key]: value }))
+  }
+
+  return <Popup open={open} handleClose={handleClose}>
+    <form onSubmit={(ev) => {ev.preventDefault(); handleClose(); closeNav()}}>
+      {/* <h2>Project settings</h2>
+      <p><i>These settings are stored in the URL as they change the project's setup</i></p>
+      <p>
+        <label htmlFor="leanVersion">Lean Project: </label>
+        <select
+            id="leanVersion"
+            name="leanVersion"
+            value={project}
+            onChange={(ev) => {
+              setProject(ev.target.value)
+              console.log(`set Lean project to: ${ev.target.value}`)
+              }} >
+          {lean4webConfig.projects.map(proj =>
+            <option key={proj.folder} value={proj.folder}>{proj.name ?? proj.folder}</option>
+          )}
+        </select>
+      </p> */}
+
+      <h2>Editor settings</h2>
+      <p>
+        <label htmlFor="abbreviationCharacter">Lead character to trigger unicode input mode</label>
+        <input id="abbreviationCharacter" type="text"
+          onChange={(ev) => {updateSetting("abbreviationCharacter", ev.target.value)}}
+          value={newSettings.abbreviationCharacter} />
+      </p>
+      <p>
+        <Switch id="wordWrap" onChange={() => {updateSetting("wordWrap", !newSettings.wordWrap)}}
+        checked={newSettings.wordWrap} />
+        <label htmlFor="wordWrap">Wrap code</label>
+      </p>
+      <p>
+        <Switch id="acceptSuggestionOnEnter" onChange={() => {updateSetting("acceptSuggestionOnEnter", !newSettings.acceptSuggestionOnEnter)}}
+        checked={newSettings.acceptSuggestionOnEnter} />
+        <label htmlFor="acceptSuggestionOnEnter">Accept Suggestion on Enter</label>
+      </p>
+      <p>
+        <Switch id="showGoalNames" onChange={() => {updateSetting("showGoalNames", !newSettings.showGoalNames)}}
+        checked={newSettings.showGoalNames} />
+        <label htmlFor="showGoalNames">Show Goal Names</label>
+      </p>
+
+      <h2>User settings</h2>
+       <p>
+        <label htmlFor="theme">Theme: </label>
+        <select
+            id="theme"
+            name="theme"
+            value={newSettings.theme}
+            onChange={(ev) => {updateSetting("theme", ev.target.value as Theme)}}
+            >
+          <option value="Visual Studio Light">visual studio light</option>
+          <option value="Visual Studio Dark">visual studio dark</option>
+          {/* <option value="Default Light+">light+</option> */}
+          {/* <option value="Default Dark+">dark+</option> */}
+          {/* <option value="Default Light Modern">light modern</option> */}
+          <option value="Default High Contrast">high contrast</option>
+          <option value="Cobalt">cobalt</option>
+
+        </select>
+      </p>
+      <div>
+        <span>Layout: </span>
+        <Box sx={{ width: 200 }}>
+          <Slider
+            value={marks.find(item => item.key === newSettings.mobile).value}
+            step={1}
+            marks={marks}
+            max={2}
+            sx={{
+              '& .MuiSlider-track': { display: 'none', },
+            }}
+            onChange={(_, val) => {
+              updateSetting("mobile", marks[val].key)
+            }}
+          />
+        </Box>
+      </div>
+      <p>
+        <Switch id="compress" onChange={() => {updateSetting("compress", !newSettings.compress)}}
+        checked={newSettings.compress} />
+        <label htmlFor="compress">Compress code in URL</label>
+      </p>
+
+      <h2>Save</h2>
+      <p><i>Editor settings and User settings are not preserved unless you opt-in to save them.</i></p>
+      <p>
+        <Switch id="savingAllowed" onChange={() => {setAllowSaveInStore(prev => !prev)}} checked={allowSaveInStore} />
+        <label htmlFor="savingAllowed">Save settings (in the browser's local storage)</label>
+      </p>
+      <p>
+        {newSettings != defaultSettings &&
+          <button id="resetSettings" onClick={e => {setNewSettings(defaultSettings); e.preventDefault()}}>Reset to Default</button>
+        }
+        <input
+          id="saveSettings"
+          type="submit"
+          value={allowSaveInStore ? "Apply & Save" : "Apply"}
+          onClick={() => {
+            if (allowSaveInStore) {
+              applyAndSaveStore(newSettings)
+            } else {
+              applyAndClearStore(newSettings)
+            }
+          }}/>
+      </p>
+    </form>
+  </Popup>
+}
+
+export default SettingsPopup
diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts
new file mode 100644
index 00000000..f5a8044c
--- /dev/null
+++ b/client/src/settings/settings-atoms.ts
@@ -0,0 +1,48 @@
+import { atomWithStorage, createJSONStorage } from 'jotai/utils'
+import { defaultSettings, Settings, SettingsStore } 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<Settings>(defaultSettings)
+
+/** User settings as they are stored in storage */
+const settingsStoreAtom = atomWithStorage<SettingsStore>('lean4web:settings', undefined, undefined, { getOnInit: true })
+
+/** The user settings  */
+export const settingsAtom = atom(get => {
+  const base = get(settingsBaseAtom)
+  const store = get(settingsStoreAtom)
+  return { ...base, ...store } 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 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)
+  console.log("store", store)
+  return store !== undefined
+})
+
+/** Indicates whether mobile layout should be used */
+export const mobileAtom = atom(
+  get => {
+    const mobile_setting = get(settingsAtom).mobile
+    if (mobile_setting === "auto") {
+      const width = get(screenWidthAtom)
+      return width < 800
+    }
+    return mobile_setting
+  }
+)
diff --git a/client/src/config/settings.ts b/client/src/settings/settings-types.ts
similarity index 69%
rename from client/src/config/settings.ts
rename to client/src/settings/settings-types.ts
index 86c6a7ce..9005a7b5 100644
--- a/client/src/config/settings.ts
+++ b/client/src/settings/settings-types.ts
@@ -6,10 +6,12 @@ Note that more Editor options are set in `App.tsx` directly.
 
 // const isBrowserDefaultDark = () => window.matchMedia('(prefers-color-scheme: dark)').matches
 
-type Theme = "Visual Studio Light" | "Visual Studio Dark"
+export type Theme = "Visual Studio Light" | "Visual Studio Dark" | "Default High Contrast" | "Cobalt"
+
+export type MobileValues = boolean | "auto"
 
 /** Type for the user settings. */
-export interface IPreferencesContext {
+export interface Settings {
   /** Lead character to trigger unicode input mode */
   abbreviationCharacter: string
   /** Accept code editors suggestions on Enter */
@@ -20,17 +22,29 @@ export interface IPreferencesContext {
   compress: boolean,
   /** Display code editor and infoview in narrow, vertically stacked, mobile-friendly mode.
    * Usually inferred from window width. */
-  mobile: boolean
-  saveInLocalStore: boolean
+  mobile: MobileValues
   /** `light` or `dark` or name of existing theme.
    * Usually inferred from browser dark mode preferences.
    */
   theme: Theme,
   /** Wrap code */
   wordWrap: boolean
+  saveInLocalStorage: 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
 }
 
-export const preferenceParams: (keyof IPreferencesContext)[] = [
+export const preferenceParams: (keyof Settings)[] = [
   "abbreviationCharacter",
   "acceptSuggestionOnEnter",
   // "compress", // not sure if this should be user-settable
@@ -41,17 +55,17 @@ export const preferenceParams: (keyof IPreferencesContext)[] = [
 ]
 
 /** The default settings. */
-const settings: IPreferencesContext = {
+export const defaultSettings: Settings = {
   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: false,
-  saveInLocalStore: false, // should be false unless user gave consent.
+  mobile: "auto",
   theme: 'Visual Studio Light', // irrelevant as it will be overwritten in App.tsx
-  wordWrap: true
+  wordWrap: true,
+  saveInLocalStorage: false,
 }
 
 /**
@@ -63,4 +77,3 @@ export const lightThemes: Theme[] = [
   'Visual Studio Light'
 ]
 
-export default settings
diff --git a/client/src/store/window-atoms.ts b/client/src/store/window-atoms.ts
new file mode 100644
index 00000000..b216b573
--- /dev/null
+++ b/client/src/store/window-atoms.ts
@@ -0,0 +1,9 @@
+import { atom } from 'jotai';
+
+/**
+ * Atom to store the screen width. Note that this atom needs to be updated with a `useEffect`
+ * in `App.tsx`.
+ */
+export const screenWidthAtom = atom(
+  window?.innerWidth ?? 1024
+);
diff --git a/cypress/e2e/settings.cy.ts b/cypress/e2e/settings.cy.ts
new file mode 100644
index 00000000..e0d458cb
--- /dev/null
+++ b/cypress/e2e/settings.cy.ts
@@ -0,0 +1,42 @@
+describe('The Settings can be changed for', () => {
+
+  it('custom lead characters', () => {
+    cy.visit('/')
+    cy.iframe().contains('All Messages (0)').should('exist')
+    cy.get('.cgmr.codicon').should('not.exist')
+    cy.get('.dropdown>.nav-link>.fa-bars').click()
+    cy.contains('.nav-link', 'Settings').click()
+    cy.get('input#abbreviationCharacter').type('{backspace}$').should('have.value', '$')
+    cy.get('button#resetSettings').should('exist')
+    cy.get('input#saveSettings').click()
+
+    cy.iframe().contains('All Messages (0)').should('exist')
+    cy.get('.cgmr.codicon').should('not.exist')
+    cy.get('div.view-line').type('example ($tau) : $tau $or $not $tau := by exact Classical.em $tau ')
+    cy.contains('div.view-line', 'example (τ) : τ ∨ ¬ τ := by exact Classical.em τ').should('exist')
+    cy.iframe().contains('No goals').should('exist').then(() => {
+      cy.contains('div.view-line span', 'τ').realHover({ position: "center" })
+      cy.contains(
+          'div.monaco-hover-content',
+          'Type τ using $ta or $tau'
+      ).should('be.visible')
+    })
+  })
+
+  it('switching themes', () => {
+    cy.visit('/')
+    cy.iframe().contains('All Messages (0)').should('exist')
+    cy.get('.monaco-editor').should('exist').invoke('css', 'background-color').then(oldBg => {
+      cy.get('.dropdown>.nav-link>.fa-bars').click()
+      cy.contains('.nav-link', 'Settings').click()
+      cy.get('select#theme').find('option:last').invoke('val').then(lastVal => {
+          cy.get('select#theme').select(lastVal)
+        })
+      cy.get('input#saveSettings').click()
+      cy.get('.monaco-editor')
+        .invoke('css', 'background-color')
+        .should('not.eq', oldBg)
+    })
+  })
+
+})
diff --git a/cypress/e2e/spec.cy.ts b/cypress/e2e/spec.cy.ts
index 688271f5..a2826f3e 100644
--- a/cypress/e2e/spec.cy.ts
+++ b/cypress/e2e/spec.cy.ts
@@ -142,42 +142,6 @@ describe('The Editor', () => {
     ]).should('exist')
   })
 
-  it('handles custom lead character', () => {
-    cy.visit('/')
-    cy.iframe().contains('All Messages (0)').should('exist')
-    cy.get('.cgmr.codicon').should('not.exist')
-    cy.get('.dropdown>.nav-link>.fa-bars').click()
-    cy.contains('.nav-link', 'Settings').click()
-    cy.get('input#abbreviationCharacter').type(`{backspace}\${enter}`)
-    cy.iframe().contains('All Messages (0)').should('exist')
-    cy.get('.cgmr.codicon').should('not.exist')
-    cy.get('div.view-line').type('example ($tau) : $tau $or $not $tau := by exact Classical.em $tau ')
-    cy.contains('div.view-line', 'example (τ) : τ ∨ ¬ τ := by exact Classical.em τ').should('exist')
-    cy.iframe().contains('No goals').should('exist').then(() => {
-      cy.contains('div.view-line span', 'τ').realHover({ position: "center" })
-      cy.contains(
-          'div.monaco-hover-content',
-          'Type τ using $ta or $tau'
-      ).should('be.visible')
-    })
-  })
-
-  it('can switch themes', () => {
-    cy.visit('/')
-    cy.iframe().contains('All Messages (0)').should('exist')
-    cy.get('.monaco-editor').should('exist').then(($editor) => {
-      const oldBg = $editor.css('background-color')
-      cy.get('.dropdown>.nav-link>.fa-bars').click()
-      cy.contains('.nav-link', 'Settings').click()
-      cy.get("select#theme option").not(':selected').first().invoke('val').then(($newVal) => {
-        cy.get("select#theme").select($newVal).should(() => {
-          const newBg = $editor.css('background-color')
-          expect(newBg).to.not.eq(oldBg)
-        })
-      })
-    })
-  })
-
   it('shows correct go-to definitions', () => {
     const isOnDarwin = Cypress.platform === 'darwin'
     const alertShown = cy.stub().as("alertShown")
diff --git a/doc/Usage.md b/doc/Usage.md
index c4c01cdb..8fb10c0b 100644
--- a/doc/Usage.md
+++ b/doc/Usage.md
@@ -25,7 +25,7 @@ logic:
 2. if the preferences say no comression, use `code`
 3. otherwise use `codez` or `code` depending on which results in a shorter URL.
 
-### URL parameters
+### URL parameters (TODO: restore behaviour)
 
 Besides storing the settings in a cookie through the settings interface, there is an option to specify them in the form `https://myserver.com/?setting1=value1&setting2=value2#[arguments as above]`
 When a setting is not provided as URL parameter, the value from the browser store (or the default) is used.
diff --git a/package-lock.json b/package-lock.json
index 3e42182a..2d951630 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -18,6 +18,8 @@
         "express": "^5.1.0",
         "file-saver": "^2.0.5",
         "ip-anonymize": "^0.1.0",
+        "jotai": "^2.16.1",
+        "jotai-react": "^0.0.0",
         "lean4monaco": "^1.1.4",
         "lz-string": "^1.5.0",
         "memfs": "^4.51.1",
@@ -58,7 +60,7 @@
       "version": "2.3.0",
       "resolved": "https://registry.npmjs.org/@ampproject/remapping/-/remapping-2.3.0.tgz",
       "integrity": "sha512-30iZtAPgz+LTIYoeivqYo853f02jBYSd5uGnGpkFV0M3xOt9aN73erkgYAmZU43x4VfqcnLxW9Kpg3R5LC4YYw==",
-      "dev": true,
+      "devOptional": true,
       "license": "Apache-2.0",
       "dependencies": {
         "@jridgewell/gen-mapping": "^0.3.5",
@@ -86,7 +88,7 @@
       "version": "7.26.8",
       "resolved": "https://registry.npmjs.org/@babel/compat-data/-/compat-data-7.26.8.tgz",
       "integrity": "sha512-oH5UPLMWR3L2wEFLnFJ1TZXqHufiTKAiLfqw5zkhS4dKXLJ10yVztfil/twG8EDTA4F/tvVNw9nOl4ZMslB8rQ==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "engines": {
         "node": ">=6.9.0"
@@ -96,7 +98,7 @@
       "version": "7.26.9",
       "resolved": "https://registry.npmjs.org/@babel/core/-/core-7.26.9.tgz",
       "integrity": "sha512-lWBYIrF7qK5+GjY5Uy+/hEgp8OJWOD/rpy74GplYRhEauvbHDeFB8t5hPOZxCZ0Oxf4Cc36tK51/l3ymJysrKw==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "peer": true,
       "dependencies": {
@@ -128,14 +130,14 @@
       "version": "2.0.0",
       "resolved": "https://registry.npmjs.org/convert-source-map/-/convert-source-map-2.0.0.tgz",
       "integrity": "sha512-Kvp459HrV2FEJ1CAsi1Ku+MY3kasH19TFykTz2xWmMeq6bk2NU3XXvfJ+Q61m0xktWwt+1HSYf3JZsTms3aRJg==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT"
     },
     "node_modules/@babel/core/node_modules/semver": {
       "version": "6.3.1",
       "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.1.tgz",
       "integrity": "sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==",
-      "dev": true,
+      "devOptional": true,
       "license": "ISC",
       "bin": {
         "semver": "bin/semver.js"
@@ -161,7 +163,7 @@
       "version": "7.26.5",
       "resolved": "https://registry.npmjs.org/@babel/helper-compilation-targets/-/helper-compilation-targets-7.26.5.tgz",
       "integrity": "sha512-IXuyn5EkouFJscIDuFF5EsiSolseme1s0CZB+QxVugqJLYmKdxI1VfIBOst0SUu4rnk2Z7kqTwmoO1lp3HIfnA==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "dependencies": {
         "@babel/compat-data": "^7.26.5",
@@ -178,7 +180,7 @@
       "version": "6.3.1",
       "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.1.tgz",
       "integrity": "sha512-BR7VvDCVHO+q2xBEWskxS6DJE1qRnb7DxzUrogb71CWoSficBxYsiAGd+Kl0mmq/MprG9yArRkyrQxTO6XjMzA==",
-      "dev": true,
+      "devOptional": true,
       "license": "ISC",
       "bin": {
         "semver": "bin/semver.js"
@@ -201,7 +203,7 @@
       "version": "7.26.0",
       "resolved": "https://registry.npmjs.org/@babel/helper-module-transforms/-/helper-module-transforms-7.26.0.tgz",
       "integrity": "sha512-xO+xu6B5K2czEnQye6BHA7DolFFmS3LB7stHZFaOLb1pAwO1HWLS8fXA+eh0A2yIvltPVmx3eNNDBJA2SLHXFw==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "dependencies": {
         "@babel/helper-module-imports": "^7.25.9",
@@ -237,7 +239,7 @@
       "version": "7.25.9",
       "resolved": "https://registry.npmjs.org/@babel/helper-validator-option/-/helper-validator-option-7.25.9.tgz",
       "integrity": "sha512-e/zv1co8pp55dNdEcCynfj9X7nyUKUXoUEwfXqaZt0omVOmDe9oOTdKStH4GmAw6zxMFs50ZayuMfHDKlO7Tfw==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "engines": {
         "node": ">=6.9.0"
@@ -247,7 +249,7 @@
       "version": "7.28.4",
       "resolved": "https://registry.npmjs.org/@babel/helpers/-/helpers-7.28.4.tgz",
       "integrity": "sha512-HFN59MmQXGHVyYadKLVumYsA9dBFun/ldYxipEjzA4196jpLZd8UjEEBLkbEkvfYreDqJhZxYAWFPtrfhNpj4w==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "dependencies": {
         "@babel/template": "^7.27.2",
@@ -286,6 +288,7 @@
       "resolved": "https://registry.npmjs.org/@babel/template/-/template-7.27.2.tgz",
       "integrity": "sha512-LPDZ85aEJyYSd18/DkjNh4/y1ntkE5KwUHWTiqgRxruuZL2F1yuHligVHLvcHY2vMHXttKFpJn6LwfI7cw7ODw==",
       "license": "MIT",
+      "peer": true,
       "dependencies": {
         "@babel/code-frame": "^7.27.1",
         "@babel/parser": "^7.27.2",
@@ -3803,7 +3806,7 @@
       "version": "4.24.4",
       "resolved": "https://registry.npmjs.org/browserslist/-/browserslist-4.24.4.tgz",
       "integrity": "sha512-KDi1Ny1gSePi1vm0q4oxSF8b4DR44GF4BbmS2YdhPLOEqd8pDviZOGH/GsmRwoWJ2+5Lr085X7naowMwKHDG1A==",
-      "dev": true,
+      "devOptional": true,
       "funding": [
         {
           "type": "opencollective",
@@ -3975,7 +3978,7 @@
       "version": "1.0.30001702",
       "resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001702.tgz",
       "integrity": "sha512-LoPe/D7zioC0REI5W73PeR1e1MLCipRGq/VkovJnd6Df+QVqT+vT33OXCp8QUd7kA7RZrHWxb1B36OQKI/0gOA==",
-      "dev": true,
+      "devOptional": true,
       "funding": [
         {
           "type": "opencollective",
@@ -4778,7 +4781,7 @@
       "version": "1.5.112",
       "resolved": "https://registry.npmjs.org/electron-to-chromium/-/electron-to-chromium-1.5.112.tgz",
       "integrity": "sha512-oen93kVyqSb3l+ziUgzIOlWt/oOuy4zRmpwestMn4rhFWAoFJeFuCVte9F2fASjeZZo7l/Cif9TiyrdW4CwEMA==",
-      "dev": true,
+      "devOptional": true,
       "license": "ISC"
     },
     "node_modules/elliptic": {
@@ -5605,7 +5608,7 @@
       "version": "1.0.0-beta.2",
       "resolved": "https://registry.npmjs.org/gensync/-/gensync-1.0.0-beta.2.tgz",
       "integrity": "sha512-3hN7NaskYvMDLQY55gnW3NQ+mesEAepTqlg+VEbj7zzqEMBVNhzcGYYeqFo/TlYz6eQiFcp1HcsCZO+nGgS8zg==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "engines": {
         "node": ">=6.9.0"
@@ -6377,6 +6380,40 @@
         "node": ">= 20"
       }
     },
+    "node_modules/jotai": {
+      "version": "2.16.1",
+      "resolved": "https://registry.npmjs.org/jotai/-/jotai-2.16.1.tgz",
+      "integrity": "sha512-vrHcAbo3P7Br37C8Bv6JshMtlKMPqqmx0DDREtTjT4nf3QChDrYdbH+4ik/9V0cXA57dK28RkJ5dctYvavcIlg==",
+      "license": "MIT",
+      "engines": {
+        "node": ">=12.20.0"
+      },
+      "peerDependencies": {
+        "@babel/core": ">=7.0.0",
+        "@babel/template": ">=7.0.0",
+        "@types/react": ">=17.0.0",
+        "react": ">=17.0.0"
+      },
+      "peerDependenciesMeta": {
+        "@babel/core": {
+          "optional": true
+        },
+        "@babel/template": {
+          "optional": true
+        },
+        "@types/react": {
+          "optional": true
+        },
+        "react": {
+          "optional": true
+        }
+      }
+    },
+    "node_modules/jotai-react": {
+      "version": "0.0.0",
+      "resolved": "https://registry.npmjs.org/jotai-react/-/jotai-react-0.0.0.tgz",
+      "integrity": "sha512-M0zXEjfwcyUVpSHJ0/iXihhPt1D14gbAnCqHqxpp7soixiwJt/i2OhqtecN3k8vHMToTSNLlA/c4vSl+xhEgCg=="
+    },
     "node_modules/js-tokens": {
       "version": "4.0.0",
       "resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz",
@@ -6469,7 +6506,7 @@
       "version": "2.2.3",
       "resolved": "https://registry.npmjs.org/json5/-/json5-2.2.3.tgz",
       "integrity": "sha512-XmOWe7eyHYH14cLdVPoyg+GOH3rYX++KpzrylJwSW98t3Nk+U8XOl8FWKOgwtzdb8lXGf6zYwDUzeHMWfxasyg==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT",
       "bin": {
         "json5": "lib/cli.js"
@@ -6769,7 +6806,7 @@
       "version": "5.1.1",
       "resolved": "https://registry.npmjs.org/lru-cache/-/lru-cache-5.1.1.tgz",
       "integrity": "sha512-KpNARQA3Iwv+jTA0utUVVbrh+Jlrr1Fv0e56GGzAFOXN7dk/FviaDW8LHmK52DlcH4WP2n6gI8vN1aesBFgo9w==",
-      "dev": true,
+      "devOptional": true,
       "license": "ISC",
       "dependencies": {
         "yallist": "^3.0.2"
@@ -7129,7 +7166,7 @@
       "version": "2.0.19",
       "resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.19.tgz",
       "integrity": "sha512-xxOWJsBKtzAq7DY0J+DTzuz58K8e7sJbdgwkbMWQe8UYB6ekmsQ45q0M/tJDsGaZmbC+l7n57UV8Hl5tHxO9uw==",
-      "dev": true,
+      "devOptional": true,
       "license": "MIT"
     },
     "node_modules/node-stdlib-browser": {
@@ -9100,7 +9137,7 @@
       "version": "1.1.3",
       "resolved": "https://registry.npmjs.org/update-browserslist-db/-/update-browserslist-db-1.1.3.tgz",
       "integrity": "sha512-UxhIZQ+QInVdunkDAaiazvvT/+fXL5Osr0JZlJulepYu6Jd7qJtDZjlur0emRlT71EN3ScPoE7gvsuIKKNavKw==",
-      "dev": true,
+      "devOptional": true,
       "funding": [
         {
           "type": "opencollective",
@@ -9644,7 +9681,7 @@
       "version": "3.1.1",
       "resolved": "https://registry.npmjs.org/yallist/-/yallist-3.1.1.tgz",
       "integrity": "sha512-a4UGQaWPH59mOXUYnAG2ewncQS4i4F43Tv3JoAM+s2VDAmS9NsK8GpDMLrCHPksFT7h3K6TOoUNn2pb7RoXx4g==",
-      "dev": true,
+      "devOptional": true,
       "license": "ISC"
     },
     "node_modules/yargs": {
diff --git a/package.json b/package.json
index 09660da4..297506a2 100644
--- a/package.json
+++ b/package.json
@@ -40,6 +40,8 @@
     "express": "^5.1.0",
     "file-saver": "^2.0.5",
     "ip-anonymize": "^0.1.0",
+    "jotai": "^2.16.1",
+    "jotai-react": "^0.0.0",
     "lean4monaco": "^1.1.4",
     "lz-string": "^1.5.0",
     "memfs": "^4.51.1",

From 36415c938c09159fb76f73652f20cbaa8e5b4937 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Sat, 27 Dec 2025 23:59:47 +0100
Subject: [PATCH 2/2] lint

---
 Projects/MathlibDemo/lake-manifest.json | 2 +-
 client/src/css/App.css                  | 5 -----
 client/src/settings/settings-atoms.ts   | 1 -
 3 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/Projects/MathlibDemo/lake-manifest.json b/Projects/MathlibDemo/lake-manifest.json
index ac70f4f7..e260cef0 100644
--- a/Projects/MathlibDemo/lake-manifest.json
+++ b/Projects/MathlibDemo/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a36c84ab8236a4869899268a42a44af07daa21ed",
+   "rev": "d68c4dc09f5e000d3c968adae8def120a0758729",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
diff --git a/client/src/css/App.css b/client/src/css/App.css
index b5f98472..d6b5bb22 100644
--- a/client/src/css/App.css
+++ b/client/src/css/App.css
@@ -36,8 +36,3 @@
 .hidden {
   display: none !important;
 }
-
-:root {
-  --vscode-editor-background: #1e1e1e;
-  --vscode-editor-foreground: #d4d4d4;
-}
\ No newline at end of file
diff --git a/client/src/settings/settings-atoms.ts b/client/src/settings/settings-atoms.ts
index f5a8044c..915ad758 100644
--- a/client/src/settings/settings-atoms.ts
+++ b/client/src/settings/settings-atoms.ts
@@ -31,7 +31,6 @@ export const applySettingsAtom = atom(null, (get, set, val) => {
 /** Indicates if there are saved settings in storage */
 export const hasSettingsSavedAtom = atom(get => {
   const store = get(settingsStoreAtom)
-  console.log("store", store)
   return store !== undefined
 })