Feat: Settings in URL

client/src/App.tsx

@@ -7,22 +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 } 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() {
@@ -38,7 +33,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<LeanMonacoOptions>({
@@ -54,7 +49,7 @@ function App() {
 
   // the user data
   const [code, setCode] = useState<string>('')
-  const [project, setProject] = useState<string>(undefined)
+  const [project, setProject] = useState<string>('MathlibDemo')
   const [url, setUrl] = useState<string | null>(null)
   const [codeFromUrl, setCodeFromUrl] = useState<string>('')
 
@@ -80,7 +75,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)
@@ -122,7 +117,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
       }
@@ -132,7 +127,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 +252,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

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<{

client/src/settings/SettingsPopup.tsx

@@ -1,77 +1,31 @@
-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 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 { 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';
+import { shallowEqualSubset } from '../utils/shallowEqual'
+import { inputAdornmentClasses } from '@mui/material/InputAdornment'
 
-// /** 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<{
+export function SettingsPopup({
+  open,
+  handleClose,
+  closeNav,
+  project,
+  setProject
+}: {
   open: boolean
   handleClose: () => void
   closeNav: () => void
   project: string
-  setProject: Dispatch<SetStateAction<string>>
-}> = ({open, handleClose, closeNav, project, setProject}) => {
-  const [hasSettingsSaved] = useAtom(hasSettingsSavedAtom)
+  setProject: (project: string) => void
+}) {
   const [settings, setSettings] = useAtom(settingsAtom)
-  const [, applyAndSaveStore] = useAtom(applyAndSaveSettingsAtom)
-  const [, applyAndClearStore] = useAtom(applySettingsAtom)
+  const [, applySettings] = 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 }))
@@ -119,6 +73,11 @@ const SettingsPopup: FC<{
         checked={newSettings.showGoalNames} />
         <label htmlFor="showGoalNames">Show Goal Names</label>
       </p>
+      <p>
+        <Switch id="showExpectedType" onChange={() => {updateSetting("showExpectedType", !newSettings.showExpectedType)}}
+        checked={newSettings.showExpectedType} />
+        <label htmlFor="showExpectedType">Show Expected Type</label>
+      </p>
 
       <h2>User settings</h2>
        <p>
@@ -143,15 +102,15 @@ const SettingsPopup: FC<{
         <span>Layout: </span>
         <Box sx={{ width: 200 }}>
           <Slider
-            value={marks.find(item => item.key === newSettings.mobile).value}
+            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)
             }}
           />
         </Box>
@@ -161,31 +120,44 @@ const SettingsPopup: FC<{
         checked={newSettings.compress} />
         <label htmlFor="compress">Compress code in URL</label>
       </p>
-
+      <p>
+        <Switch id="inUrl" onChange={() => {updateSetting("inUrl", !newSettings.inUrl)}} checked={newSettings.inUrl} />
+        <label htmlFor="inUrl">Add settings to 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} />
+        <Switch id="savingAllowed" onChange={() => {updateSetting("saved", !newSettings.saved)}} checked={newSettings.saved} />
         <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>
+        {!shallowEqualSubset(defaultSettings, newSettings) &&
+          <button id="resetSettings" onClick={e => {setNewSettings({saved: false, inUrl: false, ...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)
-            }
-          }}/>
+          value={newSettings.saved ? "Apply & Save" : "Apply"}
+          onClick={() => applySettings(newSettings)}/>
       </p>
     </form>
   </Popup>
 }
 
-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
+  },
+]

client/src/settings/settings-atoms.ts

@@ -1,37 +1,59 @@
 import { atomWithStorage, createJSONStorage } from 'jotai/utils'
-import { defaultSettings, Settings, SettingsStore } from './settings-types'
+import { defaultSettings, Settings, PartialUserSettings, 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<Settings>(defaultSettings)
+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<SettingsStore>('lean4web:settings', undefined, undefined, { getOnInit: true })
+const settingsStoreAtom = atomWithStorage<PartialUserSettings>('lean4web:settings', {}, undefined, { getOnInit: true })
+
+/** The settings which are set in the searchParams of the opened URL */
+export const settingsUrlAtom = atom<PartialUserSettings>(get => {
+  const searchParams = get(locationAtom).searchParams
+  if (!searchParams) return {}
+  return decodeSettingsFromURL(searchParams)
+})
+
+/** The settings which apply for the current session */
+const settingsBaseAtom = atom<Settings>({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 */