Compare commits
No commits in common. "3c7942494075ffe0d5c713d8aea067bd8a390a2f" and "69123b9bf02ed792595a3e0f1c3938da6c559557" have entirely different histories.
3c79424940
...
69123b9bf0
|
@ -0,0 +1,42 @@
|
|||
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,8 +15,7 @@ return {
|
|||
signcolumn = true,
|
||||
preview_config = {
|
||||
border = 'rounded'
|
||||
},
|
||||
|
||||
}
|
||||
}
|
||||
end
|
||||
}
|
||||
|
|
|
@ -14,14 +14,12 @@ 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 = {
|
||||
|
@ -43,9 +41,9 @@ return {
|
|||
git_status = {
|
||||
symbols = {
|
||||
-- Change type
|
||||
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
|
||||
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
|
||||
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 = 1,
|
||||
colwidth = 2,
|
||||
maxwidth = 1,
|
||||
condition = { true }
|
||||
},
|
||||
|
|
Loading…
Reference in New Issue