Fix code preservation of preferences change

leanprover-community · Aug 22, 2024 · 5e480b1 · 5e480b1
1 parent 51f6295
commit 5e480b1
Showing 1 changed file with 6 additions and 1 deletion.
diff --git a/client/src/App.tsx b/client/src/App.tsx
@@ -302,7 +302,12 @@ function App() {
 
   // Load content from source URL
   useEffect(() => {
-    if (!(editor && url)) { return }
+    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
+    }
     console.debug(`[Lean4web] Loading from ${url}`)
     let txt = "Loading…"
     setContent(txt)