-
Notifications
You must be signed in to change notification settings - Fork 25
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
Allow customizing infoview components via some Lua API #172
Comments
I'm not 100% sure there's a use case for this entirely (turning off widgets), it seems like instead we should just ensure we have a proper Lua API for accessing Infoview contents, and also an expansion of the components API (#172) so we may remove this config at some point.
Another consideration might be that things like the |
Another another example of a component someone may want -- "collect all |
The infoview assembles a number of subcomponents --
Tactic state,
Term state,
Diagnostic info,
Standard error output,
It may be nice to allow some customization here at some point -- such that users who want to reorder the components, or add one of their own, or change the way term or tactic state is displayed in a supported way, etc. can do so.
E.g. as a pseudo-API:
The text was updated successfully, but these errors were encountered: