Skip to content
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

Open
Tracked by #17
Julian opened this issue Oct 12, 2021 · 2 comments
Open
Tracked by #17

Allow customizing infoview components via some Lua API #172

Julian opened this issue Oct 12, 2021 · 2 comments
Labels
enhancement New feature or request infoview Relates to infoview

Comments

@Julian
Copy link
Owner

Julian commented Oct 12, 2021

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:

lean.setup{
    infoview = {components = {
        lean.infoview.components.tactic_state(),
        lean.infoview.components.term_state(),
        lean.infoview.components.diagnostic_info{ level = DiagnosticSeverity.warning },
        lean.infoview.components.server_stderr(),
    }},
}
@Julian Julian mentioned this issue Oct 12, 2021
4 tasks
@Julian Julian changed the title define a (Lua) API for configuring how goals, diagnostics and headings are assembled into the buffer contents Allow customizing infoview components via some Lua API Oct 12, 2021
@Julian Julian added enhancement New feature or request infoview Relates to infoview labels Oct 12, 2021
Julian added a commit that referenced this issue Dec 29, 2021
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.
@Julian
Copy link
Owner Author

Julian commented Jan 8, 2022

Another consideration might be that things like the filter widget in Lean 3 can take up infoview real estate. I'd love personally to hide it until/unless I WinEnter the infoview window (and possibly even then only if I hit a key). So an API here ideally would support such customization.

@Julian
Copy link
Owner Author

Julian commented Apr 14, 2022

Another another example of a component someone may want -- "collect all info-level diagnostics across all lines of the current file", rather than what we currently show, just the ones for the current line.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request infoview Relates to infoview
Projects
None yet
Development

No branches or pull requests

1 participant