-
Notifications
You must be signed in to change notification settings - Fork 1
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Expand settings window, add pedantic mode support #261
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Read through the code, loaded up the GUI and kicked the tires a little bit.
This all seems to make sense to me. I think it makes several things tidier, too.
I had a couple stray thoughts, but you can also just push as is.
}, | ||
} as const; | ||
|
||
const defaultSettings = JSON.parse( |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It occurs to me that it'd be clearer to call this "savedSettings" or "storedSettings" or something--as they aren't defaults, they're what we've saved from the user's explicitly stated preferences.
<FormControl> | ||
<FormLabel id="reset-settings"> | ||
<h3>Reset to defaults</h3> | ||
</FormLabel> | ||
<Button | ||
variant="outlined" | ||
color="error" | ||
onClick={() => { | ||
const ok = window.confirm( | ||
"Are you sure you want to clear ALL DATA (including the editors)?", | ||
); | ||
if (!ok) return; | ||
update({ type: "clear" }); | ||
localStorage.clear(); | ||
setTimeout(() => { | ||
window.location.reload(); | ||
}, 25); | ||
}} | ||
> | ||
Clear all data | ||
</Button> | ||
<FormHelperText> | ||
Reset all settings to their default values and clear the current | ||
model. <br /> | ||
Make sure to download or export your work first! | ||
</FormHelperText> | ||
</FormControl> |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Do we still want to provide this? I noted in prior versions we'd kind of talked about it as being only for development.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I like having it around still
</a>{" "} | ||
is an option in the Stan compiler to enable additional warnings. These | ||
can be instructive, but they can also lead to false positives. Be | ||
prepared to take them with a grain of salt. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have confirmed that these are warnings, and thus do not block compilation. (Which would be annoying for spurious ones, even for people who are asking for this.)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
In a fun twist, it looks like one example of a spurious error shows up in the SIR model example, where line 30 complains about a function-valued argument as being potentially uninitialized 😄
This closes #227.
User-facing changes
I expanded the compilation server selection window to be a general settings window with two tabs.
Tab One: Compilation settings (basically same as before)

Tab two: Personalization (includes dark mode, pedantic mode, and a relocated version of the "clear all" button):
Pedantic mode basically triggers a lot of additional warnings, e,g:
Internal changes
This ended up touching a lot of the code, mainly to avoid the continued expansion of the number of Contexts/Providers there are.
It introduces a UserSettings context which contains the theme, pedantic mode setting, and the compilation server that is selected. This subsumes the previous ToggleableThemeContext and part of the compilation context, which does still exist in a smaller form to provide the actual connection to the server.