mirror of
https://github.com/LazyVim/LazyVim.git
synced 2026-07-25 14:01:06 +00:00
fix: syntax
This commit is contained in:
Folke Lemaitre
parent
4b7e9e061e
commit
82573cf678
1 changed files with 102 additions and 104 deletions
|
|
@ -5,123 +5,121 @@ return {
|
||||||
root = { "lean-toolchain" },
|
root = { "lean-toolchain" },
|
||||||
})
|
})
|
||||||
end,
|
end,
|
||||||
{
|
"Julian/lean.nvim",
|
||||||
"Julian/lean.nvim",
|
event = { "BufReadPre *.lean", "BufNewFile *.lean" },
|
||||||
event = { "BufReadPre *.lean", "BufNewFile *.lean" },
|
dependencies = {
|
||||||
dependencies = {
|
"nvim-lua/plenary.nvim",
|
||||||
"nvim-lua/plenary.nvim",
|
},
|
||||||
|
|
||||||
|
-- see details below for full configuration options
|
||||||
|
opts = {
|
||||||
|
-- Enable the Lean language server(s)?
|
||||||
|
--
|
||||||
|
-- false to disable, otherwise should be a table of options to pass to `leanls`
|
||||||
|
--
|
||||||
|
-- See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls for details.
|
||||||
|
-- In particular ensure you have followed instructions setting up a callback
|
||||||
|
-- for `LspAttach` which sets your key bindings!
|
||||||
|
lsp = {
|
||||||
|
init_options = {
|
||||||
|
-- See Lean.Lsp.InitializationOptions for details and further options.
|
||||||
|
|
||||||
|
-- Time (in milliseconds) which must pass since latest edit until elaboration begins.
|
||||||
|
-- Lower values may make editing feel faster at the cost of higher CPU usage.
|
||||||
|
-- Note that lean.nvim changes the Lean default for this value!
|
||||||
|
editDelay = 0,
|
||||||
|
|
||||||
|
-- Whether to signal that widgets are supported.
|
||||||
|
hasWidgets = true,
|
||||||
|
},
|
||||||
},
|
},
|
||||||
|
|
||||||
-- see details below for full configuration options
|
ft = {
|
||||||
opts = {
|
-- A list of patterns which will be used to protect any matching
|
||||||
-- Enable the Lean language server(s)?
|
-- Lean file paths from being accidentally modified (by marking the
|
||||||
--
|
-- buffer as `nomodifiable`).
|
||||||
-- false to disable, otherwise should be a table of options to pass to `leanls`
|
nomodifiable = {
|
||||||
--
|
-- by default, this list includes the Lean standard libraries,
|
||||||
-- See https://github.com/neovim/nvim-lspconfig/blob/master/doc/server_configurations.md#leanls for details.
|
-- as well as files within dependency directories (e.g. `_target`)
|
||||||
-- In particular ensure you have followed instructions setting up a callback
|
-- Set this to an empty table to disable.
|
||||||
-- for `LspAttach` which sets your key bindings!
|
|
||||||
lsp = {
|
|
||||||
init_options = {
|
|
||||||
-- See Lean.Lsp.InitializationOptions for details and further options.
|
|
||||||
|
|
||||||
-- Time (in milliseconds) which must pass since latest edit until elaboration begins.
|
|
||||||
-- Lower values may make editing feel faster at the cost of higher CPU usage.
|
|
||||||
-- Note that lean.nvim changes the Lean default for this value!
|
|
||||||
editDelay = 0,
|
|
||||||
|
|
||||||
-- Whether to signal that widgets are supported.
|
|
||||||
hasWidgets = true,
|
|
||||||
},
|
|
||||||
},
|
},
|
||||||
|
},
|
||||||
|
|
||||||
ft = {
|
-- Abbreviation support
|
||||||
-- A list of patterns which will be used to protect any matching
|
abbreviations = {
|
||||||
-- Lean file paths from being accidentally modified (by marking the
|
-- Enable expanding of unicode abbreviations?
|
||||||
-- buffer as `nomodifiable`).
|
enable = true,
|
||||||
nomodifiable = {
|
-- additional abbreviations:
|
||||||
-- by default, this list includes the Lean standard libraries,
|
extra = {
|
||||||
-- as well as files within dependency directories (e.g. `_target`)
|
-- Add a \wknight abbreviation to insert ♘
|
||||||
-- Set this to an empty table to disable.
|
--
|
||||||
},
|
-- Note that the backslash is implied, and that you of
|
||||||
|
-- course may also use a snippet engine directly to do
|
||||||
|
-- this if so desired.
|
||||||
|
wknight = "♘",
|
||||||
},
|
},
|
||||||
|
-- Change if you don't like the backslash
|
||||||
|
-- (comma is a popular choice on French keyboards)
|
||||||
|
leader = "\\",
|
||||||
|
},
|
||||||
|
|
||||||
-- Abbreviation support
|
-- Enable suggested mappings?
|
||||||
abbreviations = {
|
--
|
||||||
-- Enable expanding of unicode abbreviations?
|
-- false by default, true to enable
|
||||||
enable = true,
|
mappings = true,
|
||||||
-- additional abbreviations:
|
|
||||||
extra = {
|
|
||||||
-- Add a \wknight abbreviation to insert ♘
|
|
||||||
--
|
|
||||||
-- Note that the backslash is implied, and that you of
|
|
||||||
-- course may also use a snippet engine directly to do
|
|
||||||
-- this if so desired.
|
|
||||||
wknight = "♘",
|
|
||||||
},
|
|
||||||
-- Change if you don't like the backslash
|
|
||||||
-- (comma is a popular choice on French keyboards)
|
|
||||||
leader = "\\",
|
|
||||||
},
|
|
||||||
|
|
||||||
-- Enable suggested mappings?
|
-- Infoview support
|
||||||
--
|
infoview = {
|
||||||
-- false by default, true to enable
|
-- Automatically open an infoview on entering a Lean buffer?
|
||||||
mappings = true,
|
-- 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.
|
||||||
|
autoopen = true,
|
||||||
|
|
||||||
-- Infoview support
|
-- Set infoview windows' starting dimensions.
|
||||||
infoview = {
|
-- Windows are opened horizontally or vertically depending on spacing.
|
||||||
-- Automatically open an infoview on entering a Lean buffer?
|
width = 50,
|
||||||
-- Should be a function that will be called anytime a new Lean file
|
height = 20,
|
||||||
-- 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.
|
|
||||||
autoopen = true,
|
|
||||||
|
|
||||||
-- Set infoview windows' starting dimensions.
|
-- Put the infoview on the top or bottom when horizontal?
|
||||||
-- Windows are opened horizontally or vertically depending on spacing.
|
-- top | bottom
|
||||||
width = 50,
|
horizontal_position = "bottom",
|
||||||
height = 20,
|
|
||||||
|
|
||||||
-- Put the infoview on the top or bottom when horizontal?
|
-- Always open the infoview window in a separate tabpage.
|
||||||
-- top | bottom
|
-- Might be useful if you are using a screen reader and don't want too
|
||||||
horizontal_position = "bottom",
|
-- many dynamic updates in the terminal at the same time.
|
||||||
|
-- Note that `height` and `width` will be ignored in this case.
|
||||||
|
separate_tab = false,
|
||||||
|
|
||||||
-- Always open the infoview window in a separate tabpage.
|
-- Show indicators for pin locations when entering an infoview window?
|
||||||
-- Might be useful if you are using a screen reader and don't want too
|
-- always | never | auto (= only when there are multiple pins)
|
||||||
-- many dynamic updates in the terminal at the same time.
|
indicators = "auto",
|
||||||
-- Note that `height` and `width` will be ignored in this case.
|
},
|
||||||
separate_tab = false,
|
|
||||||
|
|
||||||
-- Show indicators for pin locations when entering an infoview window?
|
-- Progress bar support
|
||||||
-- always | never | auto (= only when there are multiple pins)
|
progress_bars = {
|
||||||
indicators = "auto",
|
-- Enable the progress bars?
|
||||||
},
|
enable = true,
|
||||||
|
-- What character should be used for the bars?
|
||||||
|
character = "│",
|
||||||
|
-- Use a different priority for the signs
|
||||||
|
priority = 10,
|
||||||
|
},
|
||||||
|
|
||||||
-- Progress bar support
|
-- Redirect Lean's stderr messages somehwere (to a buffer by default)
|
||||||
progress_bars = {
|
stderr = {
|
||||||
-- Enable the progress bars?
|
enable = true,
|
||||||
enable = true,
|
-- height of the window
|
||||||
-- What character should be used for the bars?
|
height = 5,
|
||||||
character = "│",
|
-- a callback which will be called with (multi-line) stderr output
|
||||||
-- Use a different priority for the signs
|
-- e.g., use:
|
||||||
priority = 10,
|
-- on_lines = function(lines) vim.notify(lines) end
|
||||||
},
|
-- if you want to redirect stderr to `vim.notify`.
|
||||||
|
-- The default implementation will redirect to a dedicated stderr
|
||||||
-- Redirect Lean's stderr messages somehwere (to a buffer by default)
|
-- window.
|
||||||
stderr = {
|
on_lines = nil,
|
||||||
enable = true,
|
|
||||||
-- height of the window
|
|
||||||
height = 5,
|
|
||||||
-- a callback which will be called with (multi-line) stderr output
|
|
||||||
-- e.g., use:
|
|
||||||
-- on_lines = function(lines) vim.notify(lines) end
|
|
||||||
-- if you want to redirect stderr to `vim.notify`.
|
|
||||||
-- The default implementation will redirect to a dedicated stderr
|
|
||||||
-- window.
|
|
||||||
on_lines = nil,
|
|
||||||
},
|
|
||||||
},
|
},
|
||||||
},
|
},
|
||||||
}
|
}
|
||||||
|
|
|
||||||
Loading…
Add table
Reference in a new issue