Skip to content

Commit

Permalink
actually fix url loading
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Aug 22, 2024
1 parent 5e480b1 commit 31588dc
Showing 1 changed file with 15 additions and 13 deletions.
28 changes: 15 additions & 13 deletions client/src/App.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -278,7 +278,7 @@ function App() {
}
}, [loaded, project, preferences, options, infoviewRef, editorRef])

// Read the URL once
// Read the URL arguments once
useEffect(() => {
if (!editor) { return }
console.debug('[Lean4web] editor is ready')
Expand All @@ -302,28 +302,30 @@ function App() {

// Load content from source URL
useEffect(() => {
if (!editor || !url || code || codeFromUrl) {
// Do not execute if editor is not ready, if there is no URL to parse
// or if the editor already has some code loaded
// (last point is important for when settings change)
return
}
// Note: It is important that the editor is loaded because of the effect below:
// It does not want to retrigger on each editor reload, but it
// needs the editor to set the initial code. Therefore we wait loading the URL
// until we have an editor.
if (!editor || !url) {return}
console.debug(`[Lean4web] Loading from ${url}`)
let txt = "Loading…"
setContent(txt)
setCodeFromUrl(txt)
fetch(url)
.then((response) => response.text())
.then((code) => {
setContent(code)
setCodeFromUrl(code)
})
.catch( err => {
let errorTxt = `ERROR: ${err.toString()}`
setContent(errorTxt)
console.error(errorTxt)
setCodeFromUrl(errorTxt)
})
}, [editor, url])
}, [url, editor])

// `contentFromUrl` should only change on loading.
// this assumes the editor is loaded (see above)
useEffect(() => {
if (!codeFromUrl) { return }
setContent(codeFromUrl)
}, [codeFromUrl])

// keep url updated on changes
useEffect(() => {
Expand Down

0 comments on commit 31588dc

Please sign in to comment.