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.

Type: null or boolean or raw lua code

Default: null

Plugin default: true

Declared by:

plugins.lean.infoview.autopause

Type: null or boolean or raw lua code

Default: null

Plugin default: false

Declared by:

plugins.lean.infoview.height

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

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

Default: null

Plugin default: 20

Declared by:

plugins.lean.infoview.horizontalPosition

Put the infoview on the top or bottom when horizontal.

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

Default: null

Plugin default: "bottom"

Declared by:

plugins.lean.infoview.indicators

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

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

Default: null

Plugin default: "auto"

Declared by:

plugins.lean.infoview.mappings

Mappings.

Type: null or (attribute set of string)

Default: null

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";
}

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.

Type: null or boolean or raw lua code

Default: null

Plugin default: false

Declared by:

plugins.lean.infoview.showNoInfoMessage

Type: null or boolean or raw lua code

Default: null

Plugin default: false

Declared by:

plugins.lean.infoview.showProcessing

Type: null or boolean or raw lua code

Default: null

Plugin default: true

Declared by:

plugins.lean.infoview.useWidgets

Whether to use widgets.

Type: null or boolean or raw lua code

Default: null

Plugin default: true

Declared by:

plugins.lean.infoview.width

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

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

Default: null

Plugin default: 50

Declared by: