Skip to content

Commit

Permalink
fix project changing & fix some upload options
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Jul 24, 2024
1 parent d1d7071 commit 25efbe8
Show file tree
Hide file tree
Showing 9 changed files with 35 additions and 49 deletions.
28 changes: 16 additions & 12 deletions client/src/App.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -55,14 +55,22 @@ function App() {
const [url, setUrl] = useState<string|null>(null)
const [contentFromUrl, setContentFromUrl] = useState<string>('')

function setContent (code: string) {
editor?.getModel()?.setValue(code)
setCode(code)
}

// Setting up the editor and infoview
useEffect(() => {
const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" + "/" + project
console.log(`socket url: ${socketUrl}`)

const leanMonaco = new LeanMonaco()
const leanMonacoEditor = new LeanMonacoEditor()
;(async () => {
await leanMonaco.start('ws://localhost:8080/')
await leanMonaco.start(socketUrl)
leanMonaco.setInfoviewElement(infoviewRef.current!)
await leanMonacoEditor.start(codeviewRef.current!, `/project/leanweb.lean`, '')
await leanMonacoEditor.start(codeviewRef.current!, `/project/${project}.lean`, '')

setEditor(leanMonacoEditor.editor)

Expand All @@ -76,7 +84,7 @@ function App() {
leanMonacoEditor.dispose()
leanMonaco.dispose()
}
}, [])
}, [project])

// Read the URL once
useEffect(() => {
Expand All @@ -88,8 +96,7 @@ function App() {
console.debug(args)
if (args.code) {
let _code = decodeURIComponent(args.code)
editor.getModel()!.setValue(_code)
setCode(_code)
setContent(_code)
}
if (args.url) {setUrl(decodeURIComponent(args.url))}
if (args.project) {
Expand All @@ -103,20 +110,17 @@ function App() {
if (!(editor && url)) { return }
console.debug(`Loading from ${url}`)
let txt = "Loading…"
setCode(txt)
editor.getModel()!.setValue(txt)
setContent(txt)
setContentFromUrl(txt)
fetch(url)
.then((response) => response.text())
.then((code) => {
setCode(code)
editor.getModel()!.setValue(code)
setContent(code)
setContentFromUrl(code)
})
.catch( err => {
let errorTxt = `ERROR: ${err.toString()}`
setCode(errorTxt)
editor.getModel()!.setValue(errorTxt)
setContent(errorTxt)
setContentFromUrl(errorTxt)
})
}, [editor, url])
Expand Down Expand Up @@ -148,7 +152,7 @@ function App() {
<LeanLogo />
<Menu
code={code}
setCode={setCode}
setContent={setContent}
project={project}
setProject={setProject}
theme={theme}
Expand Down
21 changes: 11 additions & 10 deletions client/src/Navigation.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -83,20 +83,22 @@ const FlexibleMenu: React.FC <{
openLoad: any,
setOpenLoad: any,
loadFromUrl: any,
setCode: any,
setContent: any,
}> = ({isInDropdown = false, setOpenNav, openExample, setOpenExample, openLoad,
setOpenLoad, loadFromUrl, setCode
setOpenLoad, loadFromUrl, setContent
}) => {

const [loadUrlOpen, setLoadUrlOpen] = useState(false)
const [loadZulipOpen, setLoadZulipOpen] = useState(false)

const loadFileFromDisk = (event: React.ChangeEvent<HTMLInputElement>) => {
console.log('Triggered loading')
const fileToLoad = event.target.files![0]
var fileReader = new FileReader();
fileReader.onload = (fileLoadedEvent) => {
var textFromFileLoaded = fileLoadedEvent.target!.result as string;
// setContent(textFromFileLoaded)
console.log(`Loaded file! Content: ${textFromFileLoaded}`)
setContent(textFromFileLoaded)
}
fileReader.readAsText(fileToLoad, "UTF-8")
setOpenNav(false)
Expand All @@ -120,7 +122,6 @@ const FlexibleMenu: React.FC <{
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)}} />
Expand All @@ -129,22 +130,22 @@ const FlexibleMenu: React.FC <{
</Dropdown>
{/* {restart && <NavButton icon={faArrowRotateRight} text="Restart server" onClick={restart} />} */}
<LoadUrlPopup open={loadUrlOpen} handleClose={() => setLoadUrlOpen(false)} loadFromUrl={loadFromUrl} />
<LoadZulipPopup open={loadZulipOpen} handleClose={() => setLoadZulipOpen(false)} setCode={setCode} />
<LoadZulipPopup open={loadZulipOpen} handleClose={() => setLoadZulipOpen(false)} setContent={setContent} />
</>
}

/** The Navigation menu */
export const Menu: React.FC <{
code: string,
setCode: any,
setContent: any,
project: any,
setProject: any,
theme: any,
setTheme: any,
setUrl: any,
contentFromUrl: any,
settings: any,
}> = ({code, setCode, project, setProject, theme, setTheme, setUrl, contentFromUrl, settings}) => {
}> = ({code, setContent, project, setProject, theme, setTheme, setUrl, contentFromUrl, settings}) => {
// state for handling the dropdown menus
const [openNav, setOpenNav] = useState(false)
const [openExample, setOpenExample] = useState(false)
Expand All @@ -159,7 +160,7 @@ export const Menu: React.FC <{
console.debug('load code from url')
setUrl((oldUrl: string) => {
if (oldUrl === url) {
setCode(contentFromUrl)
setContent(contentFromUrl)
}
return url
})
Expand All @@ -177,7 +178,7 @@ export const Menu: React.FC <{
openLoad={openLoad}
setOpenLoad={setOpenLoad}
loadFromUrl={loadFromUrl}
setCode={setCode} />
setContent={setContent} />
}
<Dropdown open={openNav} setOpen={setOpenNav} icon={openNav ? faXmark : faBars} onClick={() => {setOpenExample(false); setOpenLoad(false)}}>
{ settings.verticalLayout &&
Expand All @@ -188,7 +189,7 @@ export const Menu: React.FC <{
openLoad={openLoad}
setOpenLoad={setOpenLoad}
loadFromUrl={loadFromUrl}
setCode={setCode} />
setContent={setContent} />
}
<NavButton icon={faGear} text="Settings" onClick={() => {setSettingsOpen(true)}} />
<NavButton icon={faHammer} text="Tools: Version" onClick={() => setToolsOpen(true)} />
Expand Down
6 changes: 3 additions & 3 deletions client/src/Popups/LoadZulip.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ import { Popup } from '../Navigation'
const LoadZulipPopup: React.FC<{
open: boolean
handleClose: () => void
setCode: React.Dispatch<React.SetStateAction<string>>
}> = ({open, handleClose, setCode}) => {
setContent: React.Dispatch<React.SetStateAction<string>>
}> = ({open, handleClose, setContent}) => {

const [error, setError] = React.useState('');
const textInputRef = React.useRef<HTMLTextAreaElement>(null)
Expand All @@ -28,7 +28,7 @@ const LoadZulipPopup: React.FC<{
console.log(`match: ${s}`)
return s.match(regex2)![2]}).join('\n\n-- new codeblock\n\n').trim() + '\n'
console.log(code)
setCode(code)
setContent(code)
//setError('')
handleClose()
} else {
Expand Down
3 changes: 0 additions & 3 deletions server/LeanProject/.gitignore

This file was deleted.

1 change: 0 additions & 1 deletion server/LeanProject/LeanProject.lean

This file was deleted.

4 changes: 0 additions & 4 deletions server/LeanProject/Main.lean

This file was deleted.

15 changes: 0 additions & 15 deletions server/LeanProject/lakefile.lean

This file was deleted.

1 change: 0 additions & 1 deletion server/LeanProject/lean-toolchain

This file was deleted.

5 changes: 5 additions & 0 deletions server/index.mjs
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,11 @@ function startServerProcess(project) {
}

wss.addListener("connection", function(ws, req) {
const urlRegEx = /^\/websocket\/([\w.-]+)$/
const reRes = urlRegEx.exec(req.url)
if (!reRes) { console.error(`Connection refused because of invalid URL: ${req.url}`); return; }
const project = reRes[1]

const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress)
const ps = startServerProcess(project)

Expand Down

0 comments on commit 25efbe8

Please sign in to comment.