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 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:
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: