From d132c168b30ee517549fa41603d3d203526e48ba Mon Sep 17 00:00:00 2001 From: MrTipson Date: Sat, 21 Sep 2024 18:09:42 +0200 Subject: [PATCH] Settings: sync garbage collection in the URL --- src/components/Machine.tsx | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/components/Machine.tsx b/src/components/Machine.tsx index be2c692..096c5d5 100644 --- a/src/components/Machine.tsx +++ b/src/components/Machine.tsx @@ -65,8 +65,8 @@ export default function Machine({ examples, default_program }: { examples: Infer const [settings, setSettingsOriginal] = useState(() => { const searchParams = new URLSearchParams(location.search); return { - garbage_collection: true, - eval_apply: searchParams.has("ea") || false, + garbage_collection: !searchParams.has("nogc"), + eval_apply: searchParams.has("ea"), collapse_indirections: true, bind_names: false, run_limit: 1000 @@ -81,9 +81,17 @@ export default function Machine({ examples, default_program }: { examples: Infer } else { searchParams.set("ea", ""); } - const newUrl = `${location.pathname}?${searchParams.toString()}`; - history.replaceState(null, '', newUrl); } + const gc = !searchParams.has("nogc"); + if (newSettings.garbage_collection !== gc) { + if (gc) { + searchParams.set("nogc", ""); + } else { + searchParams.delete("nogc"); + } + } + const newUrl = `${location.pathname}?${searchParams.toString()}`; + history.replaceState(null, '', newUrl); }; const isDesktop = useMediaQuery("(min-width: 768px)");