many things

leanprover-community · May 7, 2024 · c06471c · c06471c
1 parent 3cc8a85
commit c06471c
Show file tree

Hide file tree

Showing 26 changed files with 3,363 additions and 476 deletions.
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -12,14 +12,16 @@ import LoadUrlPopup from './Popups/LoadUrl';
 import LoadZulipPopup from './Popups/LoadZulip';
 
 import lean4webConfig from './config/config'
-import settings from './config/settings'
+import initialSettings from './config/settings'
+import { PreferencesContext } from './Popups/Settings'
 
 import { ReactComponent as Logo } from './assets/logo.svg'
 import { ReactComponent as ZulipIcon } from './assets/zulip.svg'
 
 import './css/App.css'
 import './css/Modal.css'
 import './css/Navigation.css'
+import { useWindowDimensions } from './window_width';
 
 const Editor = React.lazy(() => import('./Editor'))
 
@@ -64,6 +66,15 @@ const App: React.FC = () => {
   const [openExample, setOpenExample] = useState(false)
   const [openLoad, setOpenLoad] = useState(false)
 
+
+  /* Vertical layout is changeable in the settings.
+    If screen width is below 800, default to vertical layout instead. */
+  const {width, height} = useWindowDimensions()
+
+  const [settings, setSettings] = useState(initialSettings)
+  const [mobile, setMobile] = useState(width < 800)
+
+
   // state for the popups
   const [privacyOpen, setPrivacyOpen] = useState(false)
   const [toolsOpen, setToolsOpen] = useState(false)
@@ -107,6 +118,12 @@ const App: React.FC = () => {
     setOpenNav(false)
   }
 
+  // Calculate `mobile` from the settings.
+  useEffect(() => {
+    setMobile(settings.mobile == 'true' || (settings.mobile == 'auto' && width < 800))
+
+  }, [settings.mobile, width])
+
   // keep url updated on changes
   useEffect(() => {
     let _project = (project == 'mathlib-demo' ? null : project)
@@ -149,9 +166,10 @@ const App: React.FC = () => {
   }, [project])
 
   /** The menu items either appearing inside the dropdown or outside */
-  function flexibleMenu (isDropdown = false) { return <>
+  function flexibleMenu (isInDropdown = false) { return <>
     <Dropdown open={openExample} setOpen={setOpenExample} icon={faStar} text="Examples"
-        onClick={() => {setOpenLoad(false); (!isDropdown && setOpenNav(false))}}>
+        useOverlay={isInDropdown}
+        onClick={() => {setOpenLoad(false); (!isInDropdown && setOpenNav(false))}}>
       {lean4webConfig.projects.map(proj => proj.examples?.map(example =>
         <NavButton
           key={`${proj.name}-${example.name}`}
@@ -163,26 +181,28 @@ const App: React.FC = () => {
       ))}
     </Dropdown>
     <Dropdown open={openLoad} setOpen={setOpenLoad} icon={faUpload} text="Load"
-        onClick={() => {setOpenExample(false); (!isDropdown && setOpenNav(false))}}>
+        useOverlay={isInDropdown}
+        onClick={() => {setOpenExample(false); (!isInDropdown && setOpenNav(false))}}>
       <label htmlFor="file-upload" className="nav-link" >
         <FontAwesomeIcon icon={faUpload} /> Load file from disk
       </label>
       <NavButton icon={faCloudArrowUp} text="Load from URL" onClick={() => {setLoadUrlOpen(true)}} />
       <NavButton iconElement={<ZulipIcon />} text="Load Zulip Message" onClick={() => {setLoadZulipOpen(true)}} />
       <input id="file-upload" type="file" onChange={loadFileFromDisk} />
     </Dropdown>
+    {restart && <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />}
   </>}
 
   return (
     <div className={'app monaco-editor'}>
+      <PreferencesContext.Provider value={{settings, mobile}}>
       <nav>
         <Logo className='logo' />
         <div className='menu'>
-          {!settings.verticalLayout && flexibleMenu(false)}
+          {!mobile && flexibleMenu(false)}
           <Dropdown open={openNav} setOpen={setOpenNav} icon={openNav ? faXmark : faBars} onClick={() => {setOpenExample(false); setOpenLoad(false)}}>
-            {settings.verticalLayout && flexibleMenu(true)}
+            {mobile && flexibleMenu(true)}
             <NavButton icon={faGear} text="Settings" onClick={() => {setSettingsOpen(true)}} />
-            {restart && <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />}
             <NavButton icon={faHammer} text="Tools: Version" onClick={() => setToolsOpen(true)} />
             <NavButton icon={faDownload} text="Save file" onClick={() => save(content)} />
             <NavButton icon={faShield} text={'Privacy policy'} onClick={() => {setPrivacyOpen(true)}} />
@@ -194,14 +214,15 @@ const App: React.FC = () => {
           <ToolsPopup open={toolsOpen} handleClose={() => setToolsOpen(false)} />
           <LoadUrlPopup open={loadUrlOpen} handleClose={() => setLoadUrlOpen(false)} loadFromUrl={loadFromUrl} />
           <LoadZulipPopup open={loadZulipOpen} handleClose={() => setLoadZulipOpen(false)} setContent={setContent} />
-          <SettingsPopup open={settingsOpen} handleClose={() => setSettingsOpen(false)} closeNav={() => setOpenNav(false)}
+          <SettingsPopup open={settingsOpen} settings={settings} setSettings={setSettings} handleClose={() => setSettingsOpen(false)} closeNav={() => setOpenNav(false)}
             theme={theme} setTheme={setTheme} project={project} setProject={setProject} />
         </div>
       </nav>
       <Suspense fallback={<div className="loading-ring"></div>}>
         <Editor setRestart={setRestart}
           value={content} onDidChangeContent={setContent} theme={theme} project={project}/>
       </Suspense>
+      </PreferencesContext.Provider>
     </div>
   )
 }

diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -14,7 +14,6 @@ import { AbbreviationProvider } from './editor/abbreviation/AbbreviationProvider
 import { LeanTaskGutter } from './editor/taskgutter'
 import Split from 'react-split'
 import Notification from './Notification'
-import settings from './config/settings'
 import { IConnectionProvider } from 'monaco-languageclient'
 import { toSocket, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
 import { DisposingWebSocketMessageReader } from './reader'
@@ -24,6 +23,7 @@ import './css/Editor.css'
 import './editor/infoview.css'
 import './editor/vscode.css'
 import { render } from '@testing-library/react'
+import { PreferencesContext } from './Popups/Settings'
 
 monacoSetup()
 
@@ -39,6 +39,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
   const [dragging, setDragging] = useState<boolean | null>(false)
   const [restartMessage, setRestartMessage] = useState<boolean | null>(false)
 
+  const {settings, mobile} = React.useContext(PreferencesContext)
+
   useEffect(() => {
     if (['lightPlus', 'custom'].includes(theme)) {
       monaco.editor.setTheme(theme)
@@ -85,7 +87,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs',
-      wordWrap: settings.wordWrap ? "on" : "off",
+      wordWrap: settings.wordWrap,
       fontFamily: "JuliaMono",
     })
     setEditor(editor)
@@ -188,22 +190,22 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
         }}
         gutterStyle={(dimension, gutterSize, index) => {
           return {
-            'width': settings.verticalLayout ? '100%' : `${gutterSize}px`,
-            'height': settings.verticalLayout ? `${gutterSize}px` : '100%',
-            'cursor': settings.verticalLayout ? 'row-resize' : 'col-resize',
-            'margin-left': settings.verticalLayout ? 0 : `-${gutterSize}px`,
-            'margin-top': settings.verticalLayout ? `-${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={settings.verticalLayout ? [50, 50] : [70, 30]}
-        direction={settings.verticalLayout ? "vertical" : "horizontal"}
-        style={{flexDirection: settings.verticalLayout ? "column" : "row"}}>
+        sizes={mobile ? [50, 50] : [70, 30]}
+        direction={mobile ? "vertical" : "horizontal"}
+        style={{flexDirection: mobile ? "column" : "row"}}>
         <div ref={codeviewRef} className="codeview"
-          style={settings.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
+          style={mobile ? {width : '100%'} : {height: '100%'}}></div>
         <div ref={infoviewRef} className="vscode-light infoview"
-          style={settings.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
+          style={mobile ? {width : '100%'} : {height: '100%'}}></div>
       </Split>
       {restartMessage ?
         <Notification

diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx
@@ -24,27 +24,33 @@ export const Dropdown: React.FC<{
   setOpen: React.Dispatch<React.SetStateAction<boolean>>
   icon?: IconDefinition
   text?: string
+  useOverlay?: boolean
   onClick?: React.MouseEventHandler<HTMLAnchorElement>
   children?: React.ReactNode
-}> = ({open, setOpen, icon, text, onClick, children}) => {
+}> = ({open, setOpen, icon, text, useOverlay=false, onClick, children}) => {
   // note: it seems that we can just leave the `target="_blank"` and it has no
   // effect on links without a `href`. If not, add `if (href)` statement here...
 
-  return <div className='dropdown'>
+  return <><div className='dropdown'>
     <NavButton icon={icon} text={text} onClick={(ev) => {setOpen(!open); onClick(ev); ev.stopPropagation()}} />
     {open &&
-      <div className='dropdown-content' onClick={() => setOpen(false)}>
-      {children}
-      </div>}
+      <div className={`dropdown-content${open?'': ' '}`} onClick={() => setOpen(false)}>
+        {children}
+      </div>
+    }
   </div>
-
-  if (open) {
-    return <div className='dropdown'>
-      {children}
-    </div>
-  } else {
-    return <></>
+  { useOverlay && open &&
+    <div className="dropdown-overlay" onClick={(ev) => {setOpen(false); ev.stopPropagation()}}/>
   }
+  </>
+
+  // if (open) {
+  //   return <div className='dropdown'>
+  //     {children}
+  //   </div>
+  // } else {
+  //   return <></>
+  // }
 }
 
 /** A popup which overlays the entire screen. */
@@ -53,17 +59,17 @@ export const Popup: React.FC<{
   handleClose: () => void // TODO: what's the correct type?
   children?: React.ReactNode
 }> = ({open, handleClose, children}) => {
-  if (open) {
-    return <div className="modal-wrapper">
+  // if (open) {
+    return <div className={`modal-wrapper${open? '': ' hidden'}`}>
     <div className="modal-backdrop" onClick={handleClose} />
       <div className="modal">
         <div className="codicon codicon-close modal-close" onClick={handleClose}></div>
         {children}
       </div>
     </div>
-  } else {
-    // don't display closed popup
-    return <></>
-  }
+  // } else {
+  //   // don't display closed popup
+  //   return <></>
+  // }
 
 }