[red-knot] Default playground to Python 3.13 (#16952)

## Summary

Default playground to Python 3.13 if there's no setting present. Fix
errors when a setting was added / removed.
This commit is contained in:
Micha Reiser 2025-03-24 16:54:54 +01:00 committed by GitHub
parent 3a97bdf689
commit 85b7f808e1
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 64 additions and 21 deletions

View File

@ -84,15 +84,24 @@ export default function Chrome() {
setVersion(version); setVersion(version);
setWorkspace(workspace); setWorkspace(workspace);
let hasSettings = false;
for (const [name, content] of Object.entries(fetchedWorkspace.files)) { for (const [name, content] of Object.entries(fetchedWorkspace.files)) {
let handle = null; let handle = null;
if (name !== SETTINGS_FILE) { if (name === SETTINGS_FILE) {
updateOptions(workspace, content, setUpdateError);
hasSettings = true;
} else {
handle = workspace.openFile(name, content); handle = workspace.openFile(name, content);
} }
dispatchFiles({ type: "add", handle, name, content }); dispatchFiles({ type: "add", handle, name, content });
} }
if (!hasSettings) {
workspace.updateOptions(null);
}
dispatchFiles({ dispatchFiles({
type: "selectFileByName", type: "selectFileByName",
name: fetchedWorkspace.current, name: fetchedWorkspace.current,
@ -119,25 +128,12 @@ export default function Chrome() {
const handle = files.handles[files.selected]; const handle = files.handles[files.selected];
if (handle != null) { if (handle != null) {
try { updateFile(workspace, handle, source, setUpdateError);
workspace?.updateFile(handle, source);
setUpdateError(null);
} catch (error) {
setUpdateError(`Failed to update file: ${formatError(error)}`);
}
} else if (fileName === SETTINGS_FILE) { } else if (fileName === SETTINGS_FILE) {
try { updateOptions(workspace, source, setUpdateError);
const settings = JSON.parse(source);
workspace?.updateOptions(settings);
setUpdateError(null);
} catch (error) {
setUpdateError(
`Failed to update 'knot.json' options: ${formatError(error)}`,
);
}
} }
}, },
[files.selected, workspace, files.handles, fileName], [files.selected, files.handles, fileName, workspace],
); );
const handleFileClicked = useCallback((file: FileId) => { const handleFileClicked = useCallback((file: FileId) => {
@ -152,7 +148,9 @@ export default function Chrome() {
let handle = null; let handle = null;
if (name !== SETTINGS_FILE) { if (name === SETTINGS_FILE) {
updateOptions(workspace, "{}", setUpdateError);
} else {
handle = workspace.openFile(name, ""); handle = workspace.openFile(name, "");
} }
@ -165,7 +163,9 @@ export default function Chrome() {
(file: FileId) => { (file: FileId) => {
if (workspace != null) { if (workspace != null) {
const handle = files.handles[file]; const handle = files.handles[file];
if (handle != null) { if (handle == null) {
updateOptions(workspace, null, setUpdateError);
} else {
workspace.closeFile(handle); workspace.closeFile(handle);
} }
} }
@ -183,11 +183,15 @@ export default function Chrome() {
const handle = files.handles[file]; const handle = files.handles[file];
let newHandle: FileHandle | null = null; let newHandle: FileHandle | null = null;
if (handle != null) { if (handle == null) {
updateOptions(workspace, null, setUpdateError);
} else {
workspace.closeFile(handle); workspace.closeFile(handle);
} }
if (newName !== SETTINGS_FILE) { if (newName === SETTINGS_FILE) {
updateOptions(workspace, files.contents[file], setUpdateError);
} else {
newHandle = workspace.openFile(newName, files.contents[file]); newHandle = workspace.openFile(newName, files.contents[file]);
} }
@ -267,6 +271,7 @@ export default function Chrome() {
<PanelGroup id="vertical" direction="vertical"> <PanelGroup id="vertical" direction="vertical">
<Panel minSize={10} className="my-2" order={0}> <Panel minSize={10} className="my-2" order={0}>
<Editor <Editor
key={fileName}
theme={theme} theme={theme}
visible={true} visible={true}
fileName={fileName ?? "lib.py"} fileName={fileName ?? "lib.py"}
@ -648,3 +653,41 @@ function formatError(error: unknown): string {
? message.slice("Error: ".length) ? message.slice("Error: ".length)
: message; : message;
} }
function updateOptions(
workspace: Workspace | null,
content: string | null,
setError: (error: string | null) => void,
) {
if (workspace == null) {
return;
}
content = content ?? DEFAULT_SETTINGS;
try {
const settings = JSON.parse(content);
workspace?.updateOptions(settings);
setError(null);
} catch (error) {
setError(`Failed to update 'knot.json' options: ${formatError(error)}`);
}
}
function updateFile(
workspace: Workspace | null,
handle: FileHandle,
content: string,
setError: (error: string | null) => void,
) {
if (workspace == null) {
return;
}
try {
workspace.updateFile(handle, content);
setError(null);
} catch (error) {
setError(`Failed to update file: ${formatError(error)}`);
}
}