change contentFromUrl into codeFromUrl

leanprover-community · Aug 22, 2024 · 51f6295 · 51f6295
1 parent 9d1b7fe
commit 51f6295
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -83,7 +83,7 @@ function App() {
   const [code, setCode] = useState<string>('')
   const [project, setProject] = useState<string>('mathlib-demo')
   const [url, setUrl] = useState<string|null>(null)
-  const [contentFromUrl, setContentFromUrl] = useState<string>('')
+  const [codeFromUrl, setCodeFromUrl] = useState<string>('')
   const { width } = useWindowDimensions()
 
   // Lean4monaco options
@@ -306,25 +306,25 @@ function App() {
     console.debug(`[Lean4web] Loading from ${url}`)
     let txt = "Loading…"
     setContent(txt)
-    setContentFromUrl(txt)
+    setCodeFromUrl(txt)
     fetch(url)
     .then((response) => response.text())
     .then((code) => {
       setContent(code)
-      setContentFromUrl(code)
+      setCodeFromUrl(code)
     })
     .catch( err => {
       let errorTxt = `ERROR: ${err.toString()}`
       setContent(errorTxt)
-      setContentFromUrl(errorTxt)
+      setCodeFromUrl(errorTxt)
     })
   }, [editor, url])
 
   // keep url updated on changes
   useEffect(() => {
     if (!editor) { return }
     let _project = (project == 'mathlib-demo' ? null : project)
-    if (code === contentFromUrl) {
+    if (code === codeFromUrl) {
       if (url !== null) {
         let args = {project: _project, url: encodeURIComponent(url), code: null, codez: null}
         history.replaceState(undefined, undefined!, formatArgs(args))
@@ -351,7 +351,7 @@ function App() {
       let args = {project: _project, url: null, code: fixedEncodeURIComponent(code), codez: null}
       history.replaceState(undefined, undefined!, formatArgs(args))
     }
-  }, [editor, project, code, contentFromUrl])
+  }, [editor, project, code, codeFromUrl])
 
   return (
     <PreferencesContext.Provider value={{preferences, setPreferences}}>
@@ -364,7 +364,7 @@ function App() {
             project={project}
             setProject={setProject}
             setUrl={setUrl}
-            contentFromUrl={contentFromUrl}
+            codeFromUrl={codeFromUrl}
             restart={restart}
             codeMirror={codeMirror}
             setCodeMirror={setCodeMirror}

diff --git a/client/src/Navigation.tsx b/client/src/Navigation.tsx
@@ -139,11 +139,11 @@ export const Menu: FC <{
   project: string,
   setProject: Dispatch<SetStateAction<string>>,
   setUrl: Dispatch<SetStateAction<string | null>>,
-  contentFromUrl: string,
+  codeFromUrl: string,
   restart: () => void,
   codeMirror: boolean,
   setCodeMirror: Dispatch<SetStateAction<boolean>>,
-}> = ({code, setContent, project, setProject, setUrl, contentFromUrl, restart, codeMirror, setCodeMirror}) => {
+}> = ({code, setContent, project, setProject, setUrl, codeFromUrl, restart, codeMirror, setCodeMirror}) => {
   // state for handling the dropdown menus
   const [openNav, setOpenNav] = useState(false)
   const [openExample, setOpenExample] = useState(false)
@@ -162,7 +162,7 @@ export const Menu: FC <{
     console.debug('load code from url')
     setUrl((oldUrl: string|null) => {
       if (oldUrl === url) {
-        setContent(contentFromUrl)
+        setContent(codeFromUrl)
       }
       return url
     })