Julian / Julian/lean.nvim

Allow customizing infoview components via some Lua API

Open
#172 2 comments 0 reactions 0 assignees View on GitHub
enhancement infoview
Dominant language
Lua
Stars
581
Forks
60
Avg merge
4d 12h
Merged PRs (30d)
2

Description

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(),
}},
}
```

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.