plugins.lean.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.

Plugin default: true

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.autopause

Plugin default: false

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.height

Set infoview windows’ starting height. Windows are opened horizontally or vertically depending on spacing.

Plugin default: 20

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

Default: null

Declared by:

plugins.lean.infoview.horizontalPosition

Put the infoview on the top or bottom when horizontal.

Plugin default: "bottom"

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

Default: null

Declared by:

plugins.lean.infoview.indicators

Show indicators for pin locations when entering an infoview window. "auto" = only when there are multiple pins.

Plugin default: "auto"

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

Default: null

Declared by:

plugins.lean.infoview.mappings

Mappings.

Plugin default:

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

Type: null or (attribute set of string)

Default: null

Declared by:

plugins.lean.infoview.separateTab

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.

Plugin default: false

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.showNoInfoMessage

Plugin default: false

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.showProcessing

Plugin default: true

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.useWidgets

Whether to use widgets.

Plugin default: true

Type: null or boolean or raw lua code

Default: null

Declared by:

plugins.lean.infoview.width

Set infoview windows’ starting width. Windows are opened horizontally or vertically depending on spacing.

Plugin default: 50

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

Default: null

Declared by: