search

Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
285 stars 26 forks source link

Allow customizing infoview components via some Lua API #172

Open Julian opened 3 years ago

Julian commented 3 years ago

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 commented 2 years ago

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 commented 2 years ago

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.