cleanup App.tsx and config

leanprover-community · May 2, 2024 · 013dbad · 013dbad
1 parent 5e2ea46
commit 013dbad
Show file tree

Hide file tree

Showing 11 changed files with 99 additions and 92 deletions.
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -11,8 +11,8 @@ import ToolsPopup from './Popups/Tools';
 import LoadUrlPopup from './Popups/LoadUrl';
 import LoadZulipPopup from './Popups/LoadZulip';
 
-import * as lean4webConfig from './config.json'
-import { config } from './config/config'
+import lean4webConfig from './config/config'
+import settings from './config/settings'
 
 import { ReactComponent as Logo } from './assets/logo.svg'
 import { ReactComponent as ZulipIcon } from './assets/zulip.svg'
@@ -56,8 +56,8 @@ const save = (content: string) => {
   saveAs(blob, "Lean4WebDownload.lean");
 }
 
+/** The main application */
 const App: React.FC = () => {
-  const [restart, setRestart] = useState<(project?) => Promise<void>>()
 
   // state for handling the dropdown menus
   const [openNav, setOpenNav] = useState(false)
@@ -71,19 +71,19 @@ const App: React.FC = () => {
   const [loadUrlOpen, setLoadUrlOpen] = useState(false)
   const [loadZulipOpen, setLoadZulipOpen] = useState(false)
 
+  // the restart function is only available once the editor is loaded
+  const [restart, setRestart] = useState<(project?) => Promise<void>>()
+
   /* Option to change themes */
   const isBrowserDefaultDark = () => window.matchMedia('(prefers-color-scheme: dark)').matches
   const [theme, setTheme] = React.useState(isBrowserDefaultDark() ? 'GithubDark' : 'lightPlus')
 
+  // the data
   const [content, setContent] = useState<string>('')
-  const [url, setUrl] = useState<string>(null)
   const [project, setProject] = useState<string>('mathlib-demo')
+  const [url, setUrl] = useState<string>(null)
   const [contentFromUrl, setContentFromUrl] = useState<string>(null)
 
-  const onDidChangeContent = (newContent) => {
-    setContent(newContent)
-  }
-
   const loadFromUrl = (url: string, project=null) => {
     setUrl((oldUrl) => {
       if (oldUrl === url) {
@@ -96,12 +96,7 @@ const App: React.FC = () => {
     }
   }
 
-  const load = (file, project=null) => {
-    loadFromUrl(`${window.location.origin}/examples/${file}`, project)
-    setOpenNav(false)
-  }
-
-  const loadFileFromDisk = (event) => {
+  const loadFileFromDisk = (event: React.ChangeEvent<HTMLInputElement>) => {
     const fileToLoad = event.target.files[0]
     var fileReader = new FileReader();
     fileReader.onload = (fileLoadedEvent) => {
@@ -112,6 +107,7 @@ const App: React.FC = () => {
     setOpenNav(false)
   }
 
+  // keep url updated on changes
   useEffect(() => {
     let _project = (project == 'mathlib-demo' ? null : project)
     if (content === contentFromUrl) {
@@ -126,6 +122,7 @@ const App: React.FC = () => {
     }
   }, [project, content])
 
+  // load content from url
   useEffect(() => {
     if (url !== null) {
       setContent("Loading...")
@@ -143,21 +140,26 @@ const App: React.FC = () => {
     }
   }, [url])
 
+  // load different project
   useEffect(() => {
     if (restart) {
       console.log(`changing Lean version to ${project}`)
       restart(project)
     }
   }, [project])
 
+  /** The menu items either appearing inside the dropdown or outside */
   function flexibleMenu (isDropdown = false) { return <>
     <Dropdown open={openExample} setOpen={setOpenExample} icon={faStar} text="Examples"
         onClick={() => {setOpenLoad(false); (!isDropdown && setOpenNav(false))}}>
       {lean4webConfig.projects.map(proj => proj.examples?.map(example =>
         <NavButton
           key={`${proj.name}-${example.name}`}
           icon={faStar} text={example.name}
-          onClick={() => {load(`${proj.folder}/${example.file}`, proj.folder); setOpenExample(false)}} />
+          onClick={() => {
+            loadFromUrl(`${window.location.origin}/examples/${proj.folder}/${example.file}`, proj.folder);
+            setOpenExample(false)
+          }} />
       ))}
     </Dropdown>
     <Dropdown open={openLoad} setOpen={setOpenLoad} icon={faUpload} text="Load"
@@ -176,11 +178,11 @@ const App: React.FC = () => {
       <nav>
         <Logo className='logo' />
         <div className='menu'>
-          {!config.verticalLayout && flexibleMenu(false)}
+          {!settings.verticalLayout && flexibleMenu(false)}
           <Dropdown open={openNav} setOpen={setOpenNav} icon={openNav ? faXmark : faBars} onClick={() => {setOpenExample(false); setOpenLoad(false)}}>
-            {config.verticalLayout && flexibleMenu(true)}
+            {settings.verticalLayout && flexibleMenu(true)}
             <NavButton icon={faGear} text="Settings" onClick={() => {setSettingsOpen(true)}} />
-            <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />
+            {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)}} />
@@ -190,15 +192,15 @@ const App: React.FC = () => {
           </Dropdown>
           <PrivacyPopup open={privacyOpen} handleClose={() => setPrivacyOpen(false)} />
           <ToolsPopup open={toolsOpen} handleClose={() => setToolsOpen(false)} />
-          <SettingsPopup open={settingsOpen} handleClose={() => setSettingsOpen(false)} closeNav={() => setOpenNav(false)}
-            theme={theme} setTheme={setTheme} project={project} setProject={setProject} />
           <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)}
+            theme={theme} setTheme={setTheme} project={project} setProject={setProject} />
         </div>
       </nav>
       <Suspense fallback={<div className="loading-ring"></div>}>
         <Editor setRestart={setRestart}
-          value={content} onDidChangeContent={onDidChangeContent} theme={theme} project={project}/>
+          value={content} onDidChangeContent={setContent} theme={theme} project={project}/>
       </Suspense>
     </div>
   )

diff --git a/client/src/Editor.tsx b/client/src/Editor.tsx
@@ -1,24 +1,30 @@
 import * as React from 'react'
 import { useEffect, useRef, useState } from 'react'
-import './css/Editor.css'
-import './editor/infoview.css'
-import './editor/vscode.css'
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
+
 import { loadRenderInfoview } from '@joneugster/infoview/loader'
+import { renderInfoview } from '@joneugster/infoview'
+
 import { InfoviewApi } from '@joneugster/infoview-api'
+
 import { InfoProvider } from './editor/infoview'
 import { LeanClient } from './editor/leanclient'
 import { AbbreviationRewriter } from './editor/abbreviation/rewriter/AbbreviationRewriter'
 import { AbbreviationProvider } from './editor/abbreviation/AbbreviationProvider'
 import { LeanTaskGutter } from './editor/taskgutter'
 import Split from 'react-split'
 import Notification from './Notification'
-import { config } from './config/config'
+import settings from './config/settings'
 import { IConnectionProvider } from 'monaco-languageclient'
 import { toSocket, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
 import { DisposingWebSocketMessageReader } from './reader'
 import { monacoSetup } from './monacoSetup'
 
+import './css/Editor.css'
+import './editor/infoview.css'
+import './editor/vscode.css'
+import { render } from '@testing-library/react'
+
 monacoSetup()
 
 const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: string, project: string}> =
@@ -79,7 +85,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       tabSize: 2,
       'semanticHighlighting.enabled': true,
       theme: 'vs',
-      wordWrap: config.wordWrap ? "on" : "off",
+      wordWrap: settings.wordWrap ? "on" : "off",
       fontFamily: "JuliaMono",
     })
     setEditor(editor)
@@ -89,7 +95,7 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
       model.dispose();
       abbrevRewriter.dispose();
     }
-  }, [config.wordWrap])
+  }, [settings.wordWrap])
 
   useEffect(() => {
     const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" + "/" + project
@@ -182,22 +188,22 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
         }}
         gutterStyle={(dimension, gutterSize, index) => {
           return {
-            'width': config.verticalLayout ? '100%' : `${gutterSize}px`,
-            'height': config.verticalLayout ? `${gutterSize}px` : '100%',
-            'cursor': config.verticalLayout ? 'row-resize' : 'col-resize',
-            'margin-left': config.verticalLayout ? 0 : `-${gutterSize}px`,
-            'margin-top': config.verticalLayout ? `-${gutterSize}px` : 0,
+            '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,
             'z-index': 0,
           }}}
         gutterSize={5}
         onDragStart={() => setDragging(true)} onDragEnd={() => setDragging(false)}
-        sizes={config.verticalLayout ? [50, 50] : [70, 30]}
-        direction={config.verticalLayout ? "vertical" : "horizontal"}
-        style={{flexDirection: config.verticalLayout ? "column" : "row"}}>
+        sizes={settings.verticalLayout ? [50, 50] : [70, 30]}
+        direction={settings.verticalLayout ? "vertical" : "horizontal"}
+        style={{flexDirection: settings.verticalLayout ? "column" : "row"}}>
         <div ref={codeviewRef} className="codeview"
-          style={config.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
+          style={settings.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
         <div ref={infoviewRef} className="vscode-light infoview"
-          style={config.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
+          style={settings.verticalLayout ? {width : '100%'} : {height: '100%'}}></div>
       </Split>
       {restartMessage ?
         <Notification

diff --git a/client/src/Popups/PrivacyPolicy.tsx b/client/src/Popups/PrivacyPolicy.tsx
@@ -1,6 +1,6 @@
 import * as React from 'react'
 import { Popup } from '../Navigation'
-import { text } from '../config/text'
+import lean4webConfig from '../config/config'
 
 /** The popup with the privacy policy. */
 const PrivacyPopup: React.FC<{
@@ -20,14 +20,14 @@ const PrivacyPopup: React.FC<{
       by activating the option in the settings.
     </p>
 
-    { text.serverCountry &&
-      <p>Our server is located in {text.serverCountry}.</p>
+    { lean4webConfig.serverCountry &&
+      <p>Our server is located in {lean4webConfig.serverCountry}.</p>
     }
 
-    { text.contactInformation &&
+    { lean4webConfig.contactInformation &&
       <p>
         <strong>Contact information:</strong><br/>
-        {text.contactInformation}
+        {lean4webConfig.contactInformation}
       </p>
     }
   </Popup>

diff --git a/client/src/Popups/Settings.tsx b/client/src/Popups/Settings.tsx
@@ -1,10 +1,10 @@
 import * as React from 'react'
 import { useEffect } from 'react'
-import { config } from '../config/config';
+import settings from '../config/settings';
 import Switch from '@mui/material/Switch';
 import { useWindowDimensions } from '../window_width';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
-import * as lean4webConfig from '../config.json'
+import lean4webConfig from '../config/config'
 import { Popup } from '../Navigation';
 
 const SettingsPopup: React.FC<{
@@ -17,7 +17,7 @@ const SettingsPopup: React.FC<{
   setProject
 }> = ({open, handleClose, closeNav, theme, setTheme, project, setProject}) => {
 
-  const [abbreviationCharacter, setAbbreviationCharacter] = React.useState(config.abbreviationCharacter)
+  const [abbreviationCharacter, setAbbreviationCharacter] = React.useState(settings.abbreviationCharacter)
 
   const [savingAllowed, setSavingAllowed] = React.useState(false)
 
@@ -70,10 +70,10 @@ const SettingsPopup: React.FC<{
    * variables (state)
    */
   useEffect(() => {
-    config.abbreviationCharacter = abbreviationCharacter
-    config.verticalLayout = verticalLayout
-    config.wordWrap = wordWrap
-    config.theme = theme
+    settings.abbreviationCharacter = abbreviationCharacter
+    settings.verticalLayout = verticalLayout
+    settings.wordWrap = wordWrap
+    settings.theme = theme
     if (savingAllowed) {
       window.localStorage.setItem("abbreviationCharacter", abbreviationCharacter)
       window.localStorage.setItem("verticalLayout", verticalLayout ? 'true' : 'false')

diff --git a/client/src/config.json b/client/src/config.json
diff --git a/client/src/config/config.tsx b/client/src/config/config.tsx
@@ -0,0 +1,31 @@
+import React from "react"
+
+const lean4webConfig = {
+  "projects": [
+    { "folder": "mathlib-demo",
+      "name": "Latest Mathlib",
+      "examples": [
+        { "file": "MathlibLatest/Bijection.lean",
+          "name": "Bijection" },
+        { "file": "MathlibLatest/Logic.lean",
+          "name": "Logic" },
+        { "file": "MathlibLatest/Ring.lean",
+          "name": "Ring" },
+        { "file": "MathlibLatest/Rational.lean",
+          "name": "Rational" }]},
+    { "folder": "lean4web-tools",
+      "name": "Stable Lean" },
+  ],
+  "serverCountry": "Germany",
+  "contactInformation": <>
+      <a href="https://www.math.hhu.de/lehrstuehle-/-personen-/-ansprechpartner/innen/lehrstuehle-des-mathematischen-instituts/lehrstuhl-fuer-algebraische-geometrie/team/jon-eugster">Jon Eugster</a><br />
+      Mathematisches Institut der Heinrich-Heine-Universität Düsseldorf<br />
+      Universitätsstr. 1<br />
+      40225 Düsseldorf<br />
+      Germany<br />
+      +49 211 81-12173<br />
+    </>
+
+}
+
+export default lean4webConfig
diff --git a/client/src/config/config.ts → client/src/config/settings.ts b/client/src/config/config.ts → client/src/config/settings.ts
@@ -1,6 +1,6 @@
-/* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/config.ts` */
+/* This file contains the default settings. */
 
-export const config = {
+const settings = {
   'inputModeEnabled': true,
   'abbreviationCharacter': '\\',
   'languages': ['lean4', 'lean'],
@@ -11,3 +11,5 @@ export const config = {
   'theme': 'lightPlus',
   'customTheme': '',
 }
+
+export default settings
diff --git a/client/src/config/text.tsx b/client/src/config/text.tsx
diff --git a/client/src/editor/abbreviation/AbbreviationHoverProvider.ts b/client/src/editor/abbreviation/AbbreviationHoverProvider.ts
@@ -1,7 +1,7 @@
 /* This file is based on `vscode-lean4/vscode-lean4/src/abbreviation/AbbreviationHoverProvider.ts` */
 
 import { AbbreviationProvider } from './AbbreviationProvider';
-import { config } from '../../config/config';
+import settings from '../../config/settings';
 import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
 
 /**
@@ -28,7 +28,7 @@ export class AbbreviationHoverProvider implements monaco.languages.HoverProvider
 			return undefined;
 		}
 
-		const leader = config.abbreviationCharacter;
+		const leader = settings.abbreviationCharacter;
 
 		const hoverMarkdown = allAbbrevs
 			.map(