infoview - nixvim docs

plugins.lean.settings.infoview.autoopen

Automatically open an infoview on entering a Lean buffer.

Should be a function that will be called anytime a new Lean file is opened. Return true to open an infoview, otherwise false. Setting this to true is the same as function() return true end, i.e. autoopen for any Lean file, or setting it to false is the same as function() return false end, i.e. never autoopen.

Type: null or boolean or raw lua code

Default: null

Plugin default: true

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.autopause

Set whether a new pin is automatically paused.

Type: null or boolean or raw lua code

Default: null

Plugin default: false

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.height

Set infoview windows’ starting height.

Type: null or positive integer, meaning >0, or raw lua code

Default: null

Plugin default: 20

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.horizontal_position

Put the infoview on the top or bottom when horizontal.

Type: null or one of “bottom”, “top” or raw lua code

Default: null

Plugin default: "bottom"

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.indicators

Show indicators for pin locations when entering an infoview window.

Type: null or one of “auto”, “always”, “never” or raw lua code

Default: null

Plugin default: "auto"

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.mappings

Mappings.

Type: null or (attribute set of (string or raw lua code)) or raw lua code

Default: null

Plugin default:

{
  "<CR>" = "click";
  "<Esc>" = "clear_all";
  "<LocalLeader><Tab>" = "goto_last_window";
  C = "clear_all";
  I = "mouse_enter";
  K = "click";
  gD = "go_to_decl";
  gd = "go_to_def";
  gy = "go_to_type";
  i = "mouse_leave";
}

Declared by:

<nixvim/plugins/by-name/lean>

plugins.lean.settings.infoview.separate_tab

Always open the infoview window in a separate tabpage. Might be useful if you are using a screen reader and don’t want too many dynamic updates in the terminal at the same time.

Note that height and width will be ignored in this case.

Type: null or boolean or raw lua code

Default: null

Plugin default: false

Declared by: