You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
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
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 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.
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.
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: