Compare commits
2 Commits
69123b9bf0
...
3c79424940
Author | SHA1 | Date |
---|---|---|
Sven Vogel | 3c79424940 | |
Sven Vogel | 692cbbd6ba |
|
@ -1,42 +0,0 @@
|
|||
return {
|
||||
{
|
||||
"ms-jpq/coq_nvim",
|
||||
branch = 'coq',
|
||||
build = function(_)
|
||||
vim.cmd("COQdeps")
|
||||
end,
|
||||
config = function(_,_)
|
||||
vim.cmd("COQnow -s")
|
||||
end,
|
||||
init = function(_)
|
||||
vim.g.coq_settings = {
|
||||
display = {
|
||||
ghost_text = {
|
||||
enabled = true,
|
||||
context = { "", "" },
|
||||
highlight_group = "CursorLineFold"
|
||||
},
|
||||
pum = {
|
||||
fast_close = false,
|
||||
kind_context = { " ", " " },
|
||||
source_context = { "", " " },
|
||||
},
|
||||
icons = {
|
||||
spacing = 1,
|
||||
mode = "short"
|
||||
},
|
||||
}
|
||||
}
|
||||
end,
|
||||
dependencies = {
|
||||
{
|
||||
'ms-jpq/coq.artifacts',
|
||||
branch = "artifacts"
|
||||
},
|
||||
{
|
||||
"ms-jpq/coq.thirdparty",
|
||||
branch = "3p"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
|
@ -15,7 +15,8 @@ return {
|
|||
signcolumn = true,
|
||||
preview_config = {
|
||||
border = 'rounded'
|
||||
}
|
||||
},
|
||||
|
||||
}
|
||||
end
|
||||
}
|
||||
|
|
|
@ -44,7 +44,7 @@ return {
|
|||
lualine_c = {
|
||||
{
|
||||
'branch',
|
||||
icon = ' '
|
||||
icon = ''
|
||||
},
|
||||
{
|
||||
'diff',
|
||||
|
|
|
@ -14,12 +14,14 @@ return {
|
|||
sources = {
|
||||
"filesystem",
|
||||
"buffers",
|
||||
"git_status",
|
||||
"document_symbols"
|
||||
},
|
||||
source_selector = {
|
||||
winbar = true,
|
||||
statusline = false
|
||||
},
|
||||
close_if_last_window = true,
|
||||
popup_border_style = options.ui.border,
|
||||
default_component_configs = {
|
||||
container = {
|
||||
|
@ -41,9 +43,9 @@ return {
|
|||
git_status = {
|
||||
symbols = {
|
||||
-- Change type
|
||||
added = "A", -- or "✚", but this is redundant info if you use git_status_colors on the name
|
||||
modified = "M", -- or "", but this is redundant info if you use git_status_colors on the name
|
||||
deleted = "D",-- this can only be used in the git_status source
|
||||
added = "", -- or "✚", but this is redundant info if you use git_status_colors on the name
|
||||
modified = "", -- or "", but this is redundant info if you use git_status_colors on the name
|
||||
deleted = "-",-- this can only be used in the git_status source
|
||||
renamed = "R",-- this can only be used in the git_status source
|
||||
-- Status type
|
||||
untracked = "U",
|
||||
|
|
|
@ -15,7 +15,7 @@ return {
|
|||
{
|
||||
sign = {
|
||||
name = { "Diagnostic" },
|
||||
colwidth = 2,
|
||||
colwidth = 1,
|
||||
maxwidth = 1,
|
||||
condition = { true }
|
||||
},
|
||||
|
|
Loading…
Reference in New Issue