completely rewrote neovim config
This commit is contained in:
parent
48ec97775b
commit
44625f1ccf
48 changed files with 367 additions and 736 deletions
1
nvim/.config/nvim/after/ftplugin/haskell.lua
Normal file
1
nvim/.config/nvim/after/ftplugin/haskell.lua
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
require('haskell-tools').lsp.start()
|
||||||
|
|
@ -1,2 +0,0 @@
|
||||||
au BufRead,BufNewFile *.mm set filetype=metamath
|
|
||||||
au BufRead,BufNewFile *.mma set filetype=metamath
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
require("wball.core.options")
|
require('options')
|
||||||
require("wball.core.keymaps")
|
require('keymaps')
|
||||||
|
|
||||||
require("wball.lazy")
|
require('lazy_init')
|
||||||
|
|
|
||||||
9
nvim/.config/nvim/lua/keymaps.lua
Normal file
9
nvim/.config/nvim/lua/keymaps.lua
Normal file
|
|
@ -0,0 +1,9 @@
|
||||||
|
local keymap = vim.keymap
|
||||||
|
|
||||||
|
vim.g.mapleader = ' '
|
||||||
|
vim.g.maplocalleader = ' '
|
||||||
|
|
||||||
|
keymap.set('n', 'j', 'gj')
|
||||||
|
keymap.set('n', 'k', 'gk')
|
||||||
|
keymap.set('v', 'j', 'gj')
|
||||||
|
keymap.set('v', 'k', 'gk')
|
||||||
23
nvim/.config/nvim/lua/lazy_init.lua
Normal file
23
nvim/.config/nvim/lua/lazy_init.lua
Normal file
|
|
@ -0,0 +1,23 @@
|
||||||
|
local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
|
||||||
|
if not (vim.uv or vim.loop).fs_stat(lazypath) then
|
||||||
|
local lazyrepo = "https://github.com/folke/lazy.nvim.git"
|
||||||
|
local out = vim.fn.system({ "git", "clone", "--filter=blob:none", "--branch=stable", lazyrepo, lazypath })
|
||||||
|
if vim.v.shell_error ~= 0 then
|
||||||
|
vim.api.nvim_echo({
|
||||||
|
{ "Failed to clone lazy.nvim:\n", "ErrorMsg" },
|
||||||
|
{ out, "WarningMsg" },
|
||||||
|
{ "\nPress any key to exit..." },
|
||||||
|
}, true, {})
|
||||||
|
vim.fn.getchar()
|
||||||
|
os.exit(1)
|
||||||
|
end
|
||||||
|
end
|
||||||
|
vim.opt.rtp:prepend(lazypath)
|
||||||
|
|
||||||
|
require("lazy").setup({
|
||||||
|
spec = {
|
||||||
|
{ import = 'plugins' },
|
||||||
|
{ import = 'plugins.languages' },
|
||||||
|
},
|
||||||
|
checker = { enabled = true, notify = false },
|
||||||
|
})
|
||||||
|
|
@ -13,20 +13,18 @@ opt.autoindent = true
|
||||||
opt.ignorecase = true
|
opt.ignorecase = true
|
||||||
opt.smartcase = true
|
opt.smartcase = true
|
||||||
|
|
||||||
opt.cursorline = true
|
|
||||||
|
|
||||||
opt.termguicolors = true
|
opt.termguicolors = true
|
||||||
opt.signcolumn = "yes"
|
opt.signcolumn = 'yes'
|
||||||
|
|
||||||
opt.clipboard:append("unnamedplus")
|
opt.clipboard:append('unnamedplus')
|
||||||
|
|
||||||
opt.conceallevel = 2
|
opt.conceallevel = 2
|
||||||
|
|
||||||
opt.breakindent = true
|
opt.breakindent = true
|
||||||
opt.linebreak = true
|
opt.linebreak = true
|
||||||
|
|
||||||
vim.api.nvim_create_autocmd("TermOpen", {
|
vim.api.nvim_create_autocmd('TermOpen', {
|
||||||
pattern = "*",
|
pattern = '*',
|
||||||
callback = function()
|
callback = function()
|
||||||
vim.opt.number = false
|
vim.opt.number = false
|
||||||
vim.opt.relativenumber = false
|
vim.opt.relativenumber = false
|
||||||
10
nvim/.config/nvim/lua/plugins/colors.lua
Normal file
10
nvim/.config/nvim/lua/plugins/colors.lua
Normal file
|
|
@ -0,0 +1,10 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'catppuccin/nvim',
|
||||||
|
name = 'catppuccin',
|
||||||
|
priority = 1000,
|
||||||
|
config = function()
|
||||||
|
vim.cmd.colorscheme([[catppuccin-mocha]])
|
||||||
|
end
|
||||||
|
}
|
||||||
|
}
|
||||||
55
nvim/.config/nvim/lua/plugins/completion.lua
Normal file
55
nvim/.config/nvim/lua/plugins/completion.lua
Normal file
|
|
@ -0,0 +1,55 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'hrsh7th/nvim-cmp',
|
||||||
|
dependencies = {
|
||||||
|
'hrsh7th/cmp-nvim-lsp',
|
||||||
|
'hrsh7th/cmp-buffer',
|
||||||
|
'hrsh7th/cmp-path',
|
||||||
|
'hrsh7th/cmp-cmdline',
|
||||||
|
'onsails/lspkind.nvim',
|
||||||
|
},
|
||||||
|
config = function()
|
||||||
|
local cmp = require('cmp')
|
||||||
|
local lspkind = require('lspkind')
|
||||||
|
cmp.setup({
|
||||||
|
mapping = cmp.mapping.preset.insert({
|
||||||
|
['<C-b>'] = cmp.mapping.scroll_docs(-4),
|
||||||
|
['<C-f>'] = cmp.mapping.scroll_docs(4),
|
||||||
|
['<C-Space>'] = cmp.mapping.complete(),
|
||||||
|
['<C-e>'] = cmp.mapping.abort(),
|
||||||
|
['<CR>'] = cmp.mapping.confirm({ select = true }),
|
||||||
|
}),
|
||||||
|
sources = cmp.config.sources({
|
||||||
|
{ name = 'nvim_lsp' },
|
||||||
|
}, {
|
||||||
|
{ name = 'buffer' },
|
||||||
|
}),
|
||||||
|
formatting = {
|
||||||
|
format = lspkind.cmp_format({
|
||||||
|
mode = 'symbol',
|
||||||
|
maxwidth = 50,
|
||||||
|
ellipsis_char = '...',
|
||||||
|
show_labelDetails = true,
|
||||||
|
})
|
||||||
|
}
|
||||||
|
})
|
||||||
|
|
||||||
|
cmp.setup.cmdline({ '/', '?' }, {
|
||||||
|
mapping = cmp.mapping.preset.cmdline(),
|
||||||
|
sources = {
|
||||||
|
{ name = 'buffer' }
|
||||||
|
}
|
||||||
|
})
|
||||||
|
|
||||||
|
cmp.setup.cmdline(':', {
|
||||||
|
mapping = cmp.mapping.preset.cmdline(),
|
||||||
|
sources = cmp.config.sources({
|
||||||
|
{ name = 'path' }
|
||||||
|
}, {
|
||||||
|
{ name = 'cmdline' }
|
||||||
|
}),
|
||||||
|
matching = { disallow_symbol_nonprefix_matching = false }
|
||||||
|
})
|
||||||
|
end
|
||||||
|
}
|
||||||
|
}
|
||||||
3
nvim/.config/nvim/lua/plugins/init.lua
Normal file
3
nvim/.config/nvim/lua/plugins/init.lua
Normal file
|
|
@ -0,0 +1,3 @@
|
||||||
|
return {
|
||||||
|
'nvim-lua/plenary.nvim'
|
||||||
|
}
|
||||||
23
nvim/.config/nvim/lua/plugins/keys.lua
Normal file
23
nvim/.config/nvim/lua/plugins/keys.lua
Normal file
|
|
@ -0,0 +1,23 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'folke/which-key.nvim',
|
||||||
|
event = 'VeryLazy',
|
||||||
|
config = function()
|
||||||
|
-- set up groups
|
||||||
|
local wk = require('which-key')
|
||||||
|
wk.add({
|
||||||
|
{ '<leader>f', group = 'find' },
|
||||||
|
{ '<leader>h', group = 'help' },
|
||||||
|
})
|
||||||
|
end,
|
||||||
|
keys = {
|
||||||
|
{
|
||||||
|
"<leader>?",
|
||||||
|
function()
|
||||||
|
require("which-key").show({ global = false })
|
||||||
|
end,
|
||||||
|
desc = "Buffer Local Keymaps (which-key)",
|
||||||
|
},
|
||||||
|
},
|
||||||
|
}
|
||||||
|
}
|
||||||
16
nvim/.config/nvim/lua/plugins/languages/coq.lua
Normal file
16
nvim/.config/nvim/lua/plugins/languages/coq.lua
Normal file
|
|
@ -0,0 +1,16 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'whonore/Coqtail',
|
||||||
|
init = function()
|
||||||
|
vim.g.loaded_coqtail = 1
|
||||||
|
vim.g['coqtail#supported'] = 0
|
||||||
|
end
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'tomtomjhj/coq-lsp.nvim',
|
||||||
|
opts = {
|
||||||
|
autostart = true,
|
||||||
|
},
|
||||||
|
dependencies = { 'whonore/Coqtail' }
|
||||||
|
}
|
||||||
|
}
|
||||||
7
nvim/.config/nvim/lua/plugins/languages/haskell.lua
Normal file
7
nvim/.config/nvim/lua/plugins/languages/haskell.lua
Normal file
|
|
@ -0,0 +1,7 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'mrcjkb/haskell-tools.nvim',
|
||||||
|
version = '^4',
|
||||||
|
lazy = false,
|
||||||
|
}
|
||||||
|
}
|
||||||
1
nvim/.config/nvim/lua/plugins/languages/init.lua
Normal file
1
nvim/.config/nvim/lua/plugins/languages/init.lua
Normal file
|
|
@ -0,0 +1 @@
|
||||||
|
return {}
|
||||||
7
nvim/.config/nvim/lua/plugins/languages/rust.lua
Normal file
7
nvim/.config/nvim/lua/plugins/languages/rust.lua
Normal file
|
|
@ -0,0 +1,7 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'mrcjkb/rustaceanvim',
|
||||||
|
version = '^5',
|
||||||
|
lazy = false
|
||||||
|
}
|
||||||
|
}
|
||||||
49
nvim/.config/nvim/lua/plugins/lsp.lua
Normal file
49
nvim/.config/nvim/lua/plugins/lsp.lua
Normal file
|
|
@ -0,0 +1,49 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'neovim/nvim-lspconfig',
|
||||||
|
config = function()
|
||||||
|
local capabilities = require('cmp_nvim_lsp').default_capabilities()
|
||||||
|
local lspconfig = require('lspconfig')
|
||||||
|
local wk = require('which-key')
|
||||||
|
|
||||||
|
lspconfig.ocamllsp.setup({
|
||||||
|
capabilities = capabilities
|
||||||
|
})
|
||||||
|
|
||||||
|
vim.api.nvim_create_autocmd('LspAttach', {
|
||||||
|
group = vim.api.nvim_create_augroup('UserLspConfig', {}),
|
||||||
|
callback = function(ev)
|
||||||
|
wk.add({
|
||||||
|
{ 'gD', vim.lsp.buf.declaration, desc = 'Go to declaration' },
|
||||||
|
|
||||||
|
{ '<leader>la', vim.lsp.buf.code_action, desc = 'See available code actions' },
|
||||||
|
{ '<leader>lr', vim.lsp.buf.rename, desc = 'Rename' },
|
||||||
|
{ '<leader>lf', vim.lsp.buf.format, desc = 'Format' },
|
||||||
|
{ '<leader>le', vim.diagnostic.open_float, desc = 'Show line diagnostics' },
|
||||||
|
|
||||||
|
{ '[d', vim.diagnostic.goto_prev, desc = 'Go to previous diagnostic' },
|
||||||
|
{ '[d', vim.diagnostic.goto_next, desc = 'Go to next diagnostic' },
|
||||||
|
})
|
||||||
|
end
|
||||||
|
})
|
||||||
|
end,
|
||||||
|
dependencies = {
|
||||||
|
'ray-x/lsp_signature.nvim',
|
||||||
|
'hrsh7th/nvim-cmp',
|
||||||
|
}
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'ray-x/lsp_signature.nvim',
|
||||||
|
event = 'VeryLazy',
|
||||||
|
opts = {
|
||||||
|
hind_prefix = 'λ ',
|
||||||
|
},
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'j-hui/fidget.nvim',
|
||||||
|
config = true,
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'onsails/lspkind.nvim'
|
||||||
|
}
|
||||||
|
}
|
||||||
81
nvim/.config/nvim/lua/plugins/telescope.lua
Normal file
81
nvim/.config/nvim/lua/plugins/telescope.lua
Normal file
|
|
@ -0,0 +1,81 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'nvim-telescope/telescope.nvim',
|
||||||
|
dependencies = {
|
||||||
|
'nvim-lua/plenary.nvim',
|
||||||
|
'BurntSushi/ripgrep',
|
||||||
|
'sharkdp/fd',
|
||||||
|
'nvim-tree/nvim-web-devicons',
|
||||||
|
'folke/which-key.nvim',
|
||||||
|
},
|
||||||
|
config = function()
|
||||||
|
require('telescope').setup( {
|
||||||
|
extensions = {
|
||||||
|
fzf = {
|
||||||
|
fuzzy = true,
|
||||||
|
override_generic_sorter = true,
|
||||||
|
override_file_sorter = true,
|
||||||
|
case_mode = 'smart_case',
|
||||||
|
}
|
||||||
|
}
|
||||||
|
})
|
||||||
|
require('telescope').load_extension('fzf')
|
||||||
|
end,
|
||||||
|
keys = {
|
||||||
|
{
|
||||||
|
"<leader>ff",
|
||||||
|
require('telescope.builtin').find_files,
|
||||||
|
desc = 'Telescope find files'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fg",
|
||||||
|
require('telescope.builtin').live_grep,
|
||||||
|
desc = 'Telescope live grep'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fb",
|
||||||
|
require('telescope.builtin').buffers,
|
||||||
|
desc = 'Telescope buffers'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fh",
|
||||||
|
require('telescope.builtin').help_tags,
|
||||||
|
desc = 'Telescope help tags'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fo",
|
||||||
|
require('telescope.builtin').oldfiles,
|
||||||
|
desc = 'Telescope old files'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fc",
|
||||||
|
require('telescope.builtin').commands,
|
||||||
|
desc = 'Telescope commands'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fm",
|
||||||
|
require('telescope.builtin').marks,
|
||||||
|
desc = 'Telescope marks'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fq",
|
||||||
|
require('telescope.builtin').quickfix,
|
||||||
|
desc = 'Telescope quickfix'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fl",
|
||||||
|
require('telescope.builtin').loclist,
|
||||||
|
desc = 'Telescope loclist'
|
||||||
|
},
|
||||||
|
{
|
||||||
|
"<leader>fr",
|
||||||
|
require('telescope.builtin').registers,
|
||||||
|
desc = 'Telescope registers'
|
||||||
|
},
|
||||||
|
}
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'nvim-telescope/telescope-fzf-native.nvim',
|
||||||
|
build = 'make'
|
||||||
|
}
|
||||||
|
}
|
||||||
18
nvim/.config/nvim/lua/plugins/treesitter.lua
Normal file
18
nvim/.config/nvim/lua/plugins/treesitter.lua
Normal file
|
|
@ -0,0 +1,18 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'nvim-treesitter/nvim-treesitter',
|
||||||
|
build = ':TSUpdate',
|
||||||
|
config = function()
|
||||||
|
local configs = require('nvim-treesitter.configs')
|
||||||
|
|
||||||
|
configs.setup({
|
||||||
|
ensure_installed = 'all',
|
||||||
|
highlight = { enable = true },
|
||||||
|
indent = { enable = true }
|
||||||
|
})
|
||||||
|
end
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'HiPhish/rainbow-delimiters.nvim'
|
||||||
|
}
|
||||||
|
}
|
||||||
6
nvim/.config/nvim/lua/plugins/ui.lua
Normal file
6
nvim/.config/nvim/lua/plugins/ui.lua
Normal file
|
|
@ -0,0 +1,6 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'stevearc/dressing.nvim',
|
||||||
|
opts = {},
|
||||||
|
}
|
||||||
|
}
|
||||||
51
nvim/.config/nvim/lua/plugins/utils.lua
Normal file
51
nvim/.config/nvim/lua/plugins/utils.lua
Normal file
|
|
@ -0,0 +1,51 @@
|
||||||
|
return {
|
||||||
|
{
|
||||||
|
'kylechui/nvim-surround',
|
||||||
|
version = '*',
|
||||||
|
event = 'VeryLazy',
|
||||||
|
config = true,
|
||||||
|
},
|
||||||
|
{ 'mateuszwieloch/automkdir.nvim' },
|
||||||
|
{
|
||||||
|
'NeogitOrg/neogit',
|
||||||
|
dependencies = {
|
||||||
|
'nvim-lua/plenary.nvim',
|
||||||
|
'sindrets/diffview.nvim',
|
||||||
|
'nvim-telescope/telescope.nvim',
|
||||||
|
'nvim-tree/nvim-web-devicons',
|
||||||
|
'folke/which-key.nvim',
|
||||||
|
},
|
||||||
|
config = function()
|
||||||
|
local wk = require('which-key')
|
||||||
|
local neogit = require('neogit')
|
||||||
|
wk.add({
|
||||||
|
{ '<leader>g', group = 'git' },
|
||||||
|
{ '<leader>gn', neogit.open, desc = 'Neogit' },
|
||||||
|
{ '<leader>gd', ':DiffviewOpen<CR>', desc = 'Diffview' },
|
||||||
|
})
|
||||||
|
neogit.setup({})
|
||||||
|
end
|
||||||
|
},
|
||||||
|
{
|
||||||
|
'windwp/nvim-autopairs',
|
||||||
|
event = 'InsertEnter',
|
||||||
|
dependencies = { 'hrsh7th/nvim-cmp' },
|
||||||
|
config = function()
|
||||||
|
local autopairs = require('nvim-autopairs')
|
||||||
|
|
||||||
|
autopairs.setup({
|
||||||
|
check_ts = true,
|
||||||
|
disable_filetype = { 'TelescopePrompt', 'spectre_panel', 'scheme', 'lisp', 'clojure', },
|
||||||
|
})
|
||||||
|
|
||||||
|
-- remove single-quote rule for some languages
|
||||||
|
autopairs.get_rule("'")[1].not_filetypes = { 'scheme', 'lisp', 'ocaml', 'sml', 'rust' }
|
||||||
|
|
||||||
|
local cmp_autopairs = require('nvim-autopairs.completion.cmp')
|
||||||
|
|
||||||
|
local cmp = require('cmp')
|
||||||
|
|
||||||
|
cmp.event:on('confirm_done', cmp_autopairs.on_confirm_done())
|
||||||
|
end
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
@ -1,26 +0,0 @@
|
||||||
local keymap = vim.keymap
|
|
||||||
|
|
||||||
-- set leader key to space
|
|
||||||
vim.g.mapleader = ' '
|
|
||||||
vim.g.maplocalleader = ' '
|
|
||||||
|
|
||||||
-- let <C-hjkl> move around windows
|
|
||||||
-- keymap.set('n', '<M-h>', '<C-w>h')
|
|
||||||
-- keymap.set('n', '<M-j>', '<C-w>j')
|
|
||||||
-- keymap.set('n', '<M-k>', '<C-w>k')
|
|
||||||
-- keymap.set('n', '<M-l>', '<C-w>l')
|
|
||||||
|
|
||||||
-- same with terminals
|
|
||||||
-- keymap.set('t', '<M-h>', '<C-\\><C-n><C-w>h')
|
|
||||||
-- keymap.set('t', '<M-j>', '<C-\\><C-n><C-w>j')
|
|
||||||
-- keymap.set('t', '<M-k>', '<C-\\><C-n><C-w>k')
|
|
||||||
-- keymap.set('t', '<M-l>', '<C-\\><C-n><C-w>l')
|
|
||||||
|
|
||||||
-- navigate by visual lines
|
|
||||||
keymap.set('n', 'j', 'gj')
|
|
||||||
keymap.set('n', 'k', 'gk')
|
|
||||||
keymap.set('v', 'j', 'gj')
|
|
||||||
keymap.set('v', 'k', 'gk')
|
|
||||||
|
|
||||||
-- nohl
|
|
||||||
keymap.set("n", "<leader>nh", ":nohl<CR>", { desc = "Clear highlight" })
|
|
||||||
|
|
@ -1,25 +0,0 @@
|
||||||
local lazypath = vim.fn.stdpath("data") .. "/lazy/lazy.nvim"
|
|
||||||
if not vim.loop.fs_stat(lazypath) then
|
|
||||||
vim.fn.system({
|
|
||||||
"git",
|
|
||||||
"clone",
|
|
||||||
"--filter=blob:none",
|
|
||||||
"https://github.com/folke/lazy.nvim.git",
|
|
||||||
"--branch=stable",
|
|
||||||
lazypath,
|
|
||||||
})
|
|
||||||
end
|
|
||||||
|
|
||||||
vim.opt.rtp:prepend(lazypath)
|
|
||||||
|
|
||||||
require("lazy").setup({
|
|
||||||
{ import = "wball.plugins" },
|
|
||||||
{ import = "wball.plugins.lsp" },
|
|
||||||
checker = {
|
|
||||||
enable = true,
|
|
||||||
notify = false,
|
|
||||||
},
|
|
||||||
change_detection = {
|
|
||||||
notify = false,
|
|
||||||
},
|
|
||||||
})
|
|
||||||
|
|
@ -1,24 +0,0 @@
|
||||||
return {
|
|
||||||
"windwp/nvim-autopairs",
|
|
||||||
event = { "InsertEnter" },
|
|
||||||
dependencies = {
|
|
||||||
"hrsh7th/nvim-cmp",
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local autopairs = require("nvim-autopairs")
|
|
||||||
|
|
||||||
autopairs.setup({
|
|
||||||
check_ts = true,
|
|
||||||
disable_filetype = { "TelescopePrompt", "spectre_panel", "scheme", "lisp" },
|
|
||||||
})
|
|
||||||
|
|
||||||
-- remove single-quote rule for some languages
|
|
||||||
autopairs.get_rule("'")[1].not_filetypes = { "scheme", "lisp", "ocaml", "sml", "rust" }
|
|
||||||
|
|
||||||
local cmp_autopairs = require("nvim-autopairs.completion.cmp")
|
|
||||||
|
|
||||||
local cmp = require("cmp")
|
|
||||||
|
|
||||||
cmp.event:on("confirm_done", cmp_autopairs.on_confirm_done())
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,22 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"Mofiqul/adwaita.nvim",
|
|
||||||
lazy = false,
|
|
||||||
priority = 1000,
|
|
||||||
config = function()
|
|
||||||
vim.g.adwaita_transparent = true
|
|
||||||
vim.cmd([[colorscheme adwaita]])
|
|
||||||
end
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"catppuccin/nvim",
|
|
||||||
name = "catppuccin",
|
|
||||||
priority = 1000,
|
|
||||||
config = function()
|
|
||||||
require("catppuccin").setup({
|
|
||||||
transparent_background = true,
|
|
||||||
term_colors = true
|
|
||||||
})
|
|
||||||
end
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
return {
|
|
||||||
"numToStr/Comment.nvim",
|
|
||||||
event = { "BufReadPre", "BufNewFile" },
|
|
||||||
dependencies = {
|
|
||||||
"JoosepAlviste/nvim-ts-context-commentstring",
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
require("Comment").setup({
|
|
||||||
pre_hook = require("ts_context_commentstring.integrations.comment_nvim").create_pre_hook(),
|
|
||||||
})
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,16 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"stevearc/conform.nvim",
|
|
||||||
opts = {
|
|
||||||
formatters_by_ft = {
|
|
||||||
sml = { "smlfmt" },
|
|
||||||
ocaml = { "ocamlformat" },
|
|
||||||
typst = { "typstyle" },
|
|
||||||
},
|
|
||||||
format_on_save = {
|
|
||||||
timeout_ms = 500,
|
|
||||||
lsp_format = "fallback",
|
|
||||||
},
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
return {
|
|
||||||
"stevearc/dressing.nvim",
|
|
||||||
event = "VeryLazy",
|
|
||||||
}
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
||||||
return {
|
|
||||||
"nvim-lua/plenary.nvim"
|
|
||||||
}
|
|
||||||
|
|
@ -1,18 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"Treeniks/isabelle-syn.nvim",
|
|
||||||
ft = "isabelle",
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"Treeniks/isabelle-lsp.nvim",
|
|
||||||
ft = "isabelle",
|
|
||||||
config = function()
|
|
||||||
require('isabelle-lsp').setup({
|
|
||||||
unicode_symbols = true,
|
|
||||||
isabelle_path = '/home/wball/repos/isabelle-emacs/bin/isabelle',
|
|
||||||
})
|
|
||||||
|
|
||||||
require('lspconfig').isabelle.setup({})
|
|
||||||
end
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,11 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"whonore/Coqtail"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"https://git.sr.ht/~sircmpwn/hare.vim"
|
|
||||||
},
|
|
||||||
{
|
|
||||||
"https://git.sr.ht/~torresjrjr/vim-haredoc"
|
|
||||||
},
|
|
||||||
}
|
|
||||||
|
|
@ -1,8 +0,0 @@
|
||||||
return {
|
|
||||||
'tomtomjhj/coq-lsp.nvim',
|
|
||||||
config = function()
|
|
||||||
vim.g['loaded_coqtail'] = 1
|
|
||||||
vim.g['coqtail#supported'] = 0
|
|
||||||
require('coq-lsp').setup()
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
return {
|
|
||||||
'mrcjkb/haskell-tools.nvim',
|
|
||||||
version = '^3',
|
|
||||||
ft = { 'haskell', 'lhaskell', 'cabal', 'cabalproject' },
|
|
||||||
}
|
|
||||||
|
|
@ -1,75 +0,0 @@
|
||||||
return {
|
|
||||||
"neovim/nvim-lspconfig",
|
|
||||||
event = { "BufReadPre", "BufNewFile" },
|
|
||||||
dependencies = {
|
|
||||||
"hrsh7th/cmp-nvim-lsp",
|
|
||||||
{ "antosha417/nvim-lsp-file-operations", config = true },
|
|
||||||
{ "folke/neodev.nvim", opts = {} },
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local lspconfig = require("lspconfig")
|
|
||||||
local cmp_nvim_lsp = require("cmp_nvim_lsp")
|
|
||||||
|
|
||||||
local keymap = vim.keymap
|
|
||||||
|
|
||||||
lspconfig.rust_analyzer.setup({})
|
|
||||||
lspconfig.clangd.setup({})
|
|
||||||
lspconfig.ocamllsp.setup({})
|
|
||||||
lspconfig.millet.setup({
|
|
||||||
cmd = { "millet-ls" }
|
|
||||||
})
|
|
||||||
|
|
||||||
vim.api.nvim_create_autocmd("LspAttach", {
|
|
||||||
group = vim.api.nvim_create_augroup("UserLspConfig", {}),
|
|
||||||
callback = function(ev)
|
|
||||||
local opts = { buffer = ev.buf, silent = true }
|
|
||||||
|
|
||||||
opts.desc = "Show LSP references"
|
|
||||||
keymap.set("n", "gR", "<cmd>Telescope lsp_references<CR>", opts)
|
|
||||||
|
|
||||||
opts.desc = "Go to declaration"
|
|
||||||
keymap.set("n", "gD", vim.lsp.buf.declaration, opts)
|
|
||||||
|
|
||||||
opts.desc = "Show LSP definitions"
|
|
||||||
keymap.set("n", "gd", "<cmd>Telescope lsp_definitions<CR>", opts)
|
|
||||||
|
|
||||||
opts.desc = "Show LSP implementations"
|
|
||||||
keymap.set("n", "gi", "<cmd>Telescope lsp_implementations<CR>", opts)
|
|
||||||
|
|
||||||
opts.desc = "Show LSP type definitions"
|
|
||||||
keymap.set("n", "gt", "<cmd>Telescope lsp_type_definitions<CR>", opts)
|
|
||||||
|
|
||||||
opts.desc = "See available code actions"
|
|
||||||
keymap.set({ "n", "v" }, "<leader>la", vim.lsp.buf.code_action, opts)
|
|
||||||
|
|
||||||
opts.desc = "Smart rename"
|
|
||||||
keymap.set("n", "<leader>lr", vim.lsp.buf.rename, opts)
|
|
||||||
|
|
||||||
opts.desc = "Format"
|
|
||||||
keymap.set("n", "<leader>lf", vim.lsp.buf.format, opts)
|
|
||||||
|
|
||||||
opts.desc = "Show buffer diagnostics"
|
|
||||||
keymap.set("n", "<leader>ld", "<cmd>Telescope diagnostics bufnr=0<CR>", opts)
|
|
||||||
|
|
||||||
opts.desc = "Show line diagnostics"
|
|
||||||
keymap.set("n", "<leader>le", vim.diagnostic.open_float, opts)
|
|
||||||
|
|
||||||
opts.desc = "Go to previous diagnostic"
|
|
||||||
keymap.set("n", "[d", vim.diagnostic.goto_prev, opts)
|
|
||||||
|
|
||||||
opts.desc = "Go to next diagnostic"
|
|
||||||
keymap.set("n", "]d", vim.diagnostic.goto_next, opts)
|
|
||||||
|
|
||||||
opts.desc = "LSP Hover"
|
|
||||||
keymap.set("n", "K", vim.lsp.buf.hover, opts)
|
|
||||||
|
|
||||||
opts.desc = "Restart LSP"
|
|
||||||
keymap.set("n", "<leader>ls", ":LspRestart<CR>", opts)
|
|
||||||
end,
|
|
||||||
})
|
|
||||||
|
|
||||||
vim.lsp.handlers['textDocument/hover'] = vim.lsp.with(vim.lsp.handlers.hover, { border = "single" })
|
|
||||||
|
|
||||||
vim.diagnostic.config({ virtual_text = true })
|
|
||||||
end,
|
|
||||||
}
|
|
||||||
|
|
@ -1,6 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"j-hui/fidget.nvim",
|
|
||||||
config = true,
|
|
||||||
},
|
|
||||||
}
|
|
||||||
|
|
@ -1,4 +0,0 @@
|
||||||
return {
|
|
||||||
'vxpm/ferris.nvim',
|
|
||||||
config = true,
|
|
||||||
}
|
|
||||||
|
|
@ -1,22 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"NeogitOrg/neogit",
|
|
||||||
dependencies = {
|
|
||||||
"nvim-lua/plenary.nvim",
|
|
||||||
"sindrets/diffview.nvim",
|
|
||||||
"nvim-telescope/telescope.nvim",
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local neogit = require("neogit")
|
|
||||||
vim.keymap.set("n",
|
|
||||||
"<leader>go",
|
|
||||||
function()
|
|
||||||
neogit.open({ kind="auto" })
|
|
||||||
end,
|
|
||||||
{ desc = "Open Neogit in new split" })
|
|
||||||
vim.keymap.set("n", "<leader>gg", neogit.open, { desc = "Open Neogit in new tab "})
|
|
||||||
|
|
||||||
neogit.setup()
|
|
||||||
end
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,57 +0,0 @@
|
||||||
return {
|
|
||||||
"hrsh7th/nvim-cmp",
|
|
||||||
event = "InsertEnter",
|
|
||||||
dependencies = {
|
|
||||||
"hrsh7th/cmp-buffer",
|
|
||||||
"hrsh7th/cmp-path",
|
|
||||||
{
|
|
||||||
"L3MON4D3/LuaSnip",
|
|
||||||
version = "v2.*",
|
|
||||||
},
|
|
||||||
"saadparwaiz1/cmp_luasnip",
|
|
||||||
"rafamadriz/friendly-snippets",
|
|
||||||
"onsails/lspkind.nvim",
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local cmp = require("cmp")
|
|
||||||
|
|
||||||
local luasnip = require("luasnip")
|
|
||||||
|
|
||||||
local lspkind = require("lspkind")
|
|
||||||
|
|
||||||
require("luasnip.loaders.from_vscode").lazy_load()
|
|
||||||
|
|
||||||
cmp.setup({
|
|
||||||
completion = {
|
|
||||||
completeopt = "menu,menuone,preview,noselect",
|
|
||||||
},
|
|
||||||
snippet = {
|
|
||||||
expand = function(args)
|
|
||||||
luasnip.lsp_expand(args.body)
|
|
||||||
end,
|
|
||||||
},
|
|
||||||
mapping = cmp.mapping.preset.insert({
|
|
||||||
["<C-p>"] = cmp.mapping.select_prev_item(),
|
|
||||||
["<C-n>"] = cmp.mapping.select_next_item(),
|
|
||||||
["<C-b>"] = cmp.mapping.scroll_docs(-4),
|
|
||||||
["<C-f>"] = cmp.mapping.scroll_docs(4),
|
|
||||||
["<C-Space>"] = cmp.mapping.complete(),
|
|
||||||
["<C-e>"] = cmp.mapping.abort(),
|
|
||||||
["<CR>"] = cmp.mapping.confirm({ select = false }),
|
|
||||||
}),
|
|
||||||
sources = cmp.config.sources({
|
|
||||||
{ name = "nvim_lsp" },
|
|
||||||
{ name = "luasnip" },
|
|
||||||
{ name = "buffer" },
|
|
||||||
{ name = "path" },
|
|
||||||
}),
|
|
||||||
|
|
||||||
formatting = {
|
|
||||||
format = lspkind.cmp_format({
|
|
||||||
maxwidth = 50,
|
|
||||||
ellipsis_char = "...",
|
|
||||||
}),
|
|
||||||
},
|
|
||||||
})
|
|
||||||
end,
|
|
||||||
}
|
|
||||||
|
|
@ -1,17 +0,0 @@
|
||||||
return {
|
|
||||||
"nvim-tree/nvim-tree.lua",
|
|
||||||
dependencies = "nvim-tree/nvim-web-devicons",
|
|
||||||
config = function()
|
|
||||||
local nvimtree = require("nvim-tree")
|
|
||||||
|
|
||||||
vim.g.loaded_netrw = 1
|
|
||||||
vim.g.loaded_netrwPlugin = 1
|
|
||||||
|
|
||||||
nvimtree.setup()
|
|
||||||
|
|
||||||
vim.keymap.set("n", "<leader>ee", "<cmd>NvimTreeToggle<CR>", { desc = "Toggle NvimTree" })
|
|
||||||
vim.keymap.set("n", "<leader>ef", "<cmd>NvimTreeFindFileToggle<CR>", { desc = "Toggle NvimTree on current file" })
|
|
||||||
vim.keymap.set("n", "<leader>ec", "<cmd>NvimTreeCollapse<CR>", { desc = "Collapse NvimTree" })
|
|
||||||
vim.keymap.set("n", "<leader>er", "<cmd>NvimTreeRefresh<CR>", { desc = "Refresh NvimTree" })
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,5 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
'jez/vim-better-sml'
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,6 +0,0 @@
|
||||||
return {
|
|
||||||
"kylechui/nvim-surround",
|
|
||||||
event = { "BufReadPre", "BufNewFile" },
|
|
||||||
version = "*",
|
|
||||||
config = true,
|
|
||||||
}
|
|
||||||
|
|
@ -1,36 +0,0 @@
|
||||||
return {
|
|
||||||
"nvim-telescope/telescope.nvim",
|
|
||||||
branch = "0.1.x",
|
|
||||||
dependencies = {
|
|
||||||
"nvim-lua/plenary.nvim",
|
|
||||||
{ "nvim-telescope/telescope-fzf-native.nvim", build = "make" },
|
|
||||||
"nvim-tree/nvim-web-devicons",
|
|
||||||
"folke/todo-comments.nvim",
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local telescope = require("telescope")
|
|
||||||
local actions = require("telescope.actions")
|
|
||||||
|
|
||||||
telescope.setup()
|
|
||||||
|
|
||||||
telescope.load_extension("fzf")
|
|
||||||
|
|
||||||
|
|
||||||
local builtin = require('telescope.builtin')
|
|
||||||
vim.keymap.set("n", "<leader>ff", builtin.find_files, { desc = "Fuzzy find files in cwd" })
|
|
||||||
vim.keymap.set("n", "<leader>fr", builtin.registers, { desc = "Fuzzy find registers" })
|
|
||||||
vim.keymap.set("n", "<leader>fb", builtin.buffers, { desc = "Fuzzy find buffers" })
|
|
||||||
vim.keymap.set("n", "<leader>fl", builtin.live_grep, { desc = "Live grep" })
|
|
||||||
vim.keymap.set("n", "<leader>fs", builtin.grep_string, { desc = "Grep string under cursor in cwd" })
|
|
||||||
vim.keymap.set("n", "<leader>ftt", builtin.tags, { desc = "Fuzzy find tags" })
|
|
||||||
vim.keymap.set("n", "<leader>fgf", builtin.git_files, { desc = "Fuzzy search git files" })
|
|
||||||
vim.keymap.set("n", "<leader>fgc", builtin.git_commits, { desc = "Fuzzy search git commits" })
|
|
||||||
vim.keymap.set("n", "<leader>ftb", builtin.builtin, { desc = "Search telescope builtins" })
|
|
||||||
vim.keymap.set("n", "<leader>fc", builtin.commands, { desc = "Fuzzy search commands" })
|
|
||||||
vim.keymap.set("n", "<leader>fq", builtin.quickfix, { desc = "Search quickfix list" })
|
|
||||||
vim.keymap.set("n", "<leader>fl", builtin.loclist, { desc = "Search loclist" })
|
|
||||||
vim.keymap.set("n", "<leader>fh", builtin.help_tags, { desc = "Search help tags" })
|
|
||||||
vim.keymap.set("n", "<leader>fm", builtin.marks, { desc = "Search marks" })
|
|
||||||
vim.keymap.set("n", "<leader>fd", "<cmd>TodoTelescope<cr>", { desc = "Find todos" })
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,12 +0,0 @@
|
||||||
return {
|
|
||||||
{
|
|
||||||
"akinsho/toggleterm.nvim",
|
|
||||||
opts = {
|
|
||||||
open_mapping = [[<C-\>]],
|
|
||||||
direction = "horizontal",
|
|
||||||
insert_mappings = true,
|
|
||||||
start_in_insert = true,
|
|
||||||
},
|
|
||||||
keys = [[<C-\>]],
|
|
||||||
},
|
|
||||||
}
|
|
||||||
|
|
@ -1,11 +0,0 @@
|
||||||
return {
|
|
||||||
"numToStr/Navigator.nvim",
|
|
||||||
config = function()
|
|
||||||
require('Navigator').setup()
|
|
||||||
vim.keymap.set({'n', 't'}, '<A-h>', '<CMD>NavigatorLeft<CR>')
|
|
||||||
vim.keymap.set({'n', 't'}, '<A-l>', '<CMD>NavigatorRight<CR>')
|
|
||||||
vim.keymap.set({'n', 't'}, '<A-k>', '<CMD>NavigatorUp<CR>')
|
|
||||||
vim.keymap.set({'n', 't'}, '<A-j>', '<CMD>NavigatorDown<CR>')
|
|
||||||
vim.keymap.set({'n', 't'}, '<A-p>', '<CMD>NavigatorPrevious<CR>')
|
|
||||||
end,
|
|
||||||
}
|
|
||||||
|
|
@ -1,18 +0,0 @@
|
||||||
return {
|
|
||||||
"folke/todo-comments.nvim",
|
|
||||||
event = { "BufReadPre", "BufNewFile" },
|
|
||||||
dependencies = { "nvim-lua/plenary.nvim" },
|
|
||||||
config = function()
|
|
||||||
local todo_comments = require("todo-comments")
|
|
||||||
|
|
||||||
vim.keymap.set("n", "]t", function()
|
|
||||||
todo_comments.jump_next()
|
|
||||||
end, { desc = "Next todo comment" })
|
|
||||||
|
|
||||||
vim.keymap.set("n", "[t", function()
|
|
||||||
todo_comments.jump_prev()
|
|
||||||
end, { desc = "Previous todo comment" })
|
|
||||||
|
|
||||||
todo_comments.setup()
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,30 +0,0 @@
|
||||||
return {
|
|
||||||
"nvim-treesitter/nvim-treesitter",
|
|
||||||
event = { "BufReadPre", "BufNewFile" },
|
|
||||||
build = ":TSUpdate",
|
|
||||||
dependencies = {
|
|
||||||
"HiPhish/rainbow-delimiters.nvim"
|
|
||||||
},
|
|
||||||
config = function()
|
|
||||||
local treesitter = require('nvim-treesitter.configs')
|
|
||||||
treesitter.setup({
|
|
||||||
highlight = {
|
|
||||||
enable = true,
|
|
||||||
disable = { "latex" },
|
|
||||||
},
|
|
||||||
indent = { enable = true },
|
|
||||||
|
|
||||||
ensure_installed = "all",
|
|
||||||
|
|
||||||
incremental_selection = {
|
|
||||||
enable = true,
|
|
||||||
keymaps = {
|
|
||||||
init_selection = "<C-space>",
|
|
||||||
node_incremental = "<C-space>",
|
|
||||||
scope_incremental = false,
|
|
||||||
node_decremental = "<bs>",
|
|
||||||
}
|
|
||||||
}
|
|
||||||
})
|
|
||||||
end
|
|
||||||
}
|
|
||||||
|
|
@ -1,3 +0,0 @@
|
||||||
return {
|
|
||||||
"vifm/vifm.vim",
|
|
||||||
}
|
|
||||||
|
|
@ -1,9 +0,0 @@
|
||||||
return {
|
|
||||||
"folke/which-key.nvim",
|
|
||||||
event = "VeryLazy",
|
|
||||||
init = function()
|
|
||||||
vim.o.timeout = true
|
|
||||||
vim.o.timeoutlen = 500
|
|
||||||
end,
|
|
||||||
opts = {}
|
|
||||||
}
|
|
||||||
|
|
@ -1,240 +0,0 @@
|
||||||
" Vim syntax file
|
|
||||||
" Language: Metamath
|
|
||||||
" Maintainer: David A. Wheeler <dwheeler@dwheeler.com>
|
|
||||||
" Latest Revision: 7 July 2016
|
|
||||||
" Metamath is a tiny language that can express theorems in abstract
|
|
||||||
" mathematics, accompanied by proofs that can be verified by a computer
|
|
||||||
" program with absolute rigor. For more info see: http://metamath.org/
|
|
||||||
|
|
||||||
if exists('b:current_syntax')
|
|
||||||
finish
|
|
||||||
endif
|
|
||||||
|
|
||||||
syn case match
|
|
||||||
|
|
||||||
" Synchronize display on the last-seen comment closer, for speed.
|
|
||||||
syn sync match metamathSyncComment grouphere NONE '\<$)\>'
|
|
||||||
|
|
||||||
" Whitespace and newlines delimit nearly everything.
|
|
||||||
" Identifiers can contain '.' and '$'; parentheses are valid constants.
|
|
||||||
setlocal iskeyword=33-255
|
|
||||||
|
|
||||||
" Highlight $.. commands that don't match anything else.
|
|
||||||
syn match metamathBadStatement '$[^ {}]'
|
|
||||||
|
|
||||||
" Handle special constructs within a comment.
|
|
||||||
|
|
||||||
" A cross-reference in a comment; begins with '~'.
|
|
||||||
syn region metamathXref contained
|
|
||||||
\ start='\<\~ \+'
|
|
||||||
\ end='\>'
|
|
||||||
|
|
||||||
" An expression in a comment; enclosed by `...` (backquotes).
|
|
||||||
syn region metamathEmbeddedExpression contained
|
|
||||||
\ start='\<"\?`\>'
|
|
||||||
\ end='\<`\>'
|
|
||||||
\ contains=@metamathExpression
|
|
||||||
\ skip='``'
|
|
||||||
|
|
||||||
" An date in a comment; these are common enough to visually distinguish.
|
|
||||||
syn match metamathDate contained
|
|
||||||
\ '\([1-2][0-9]\|3[0-1]\|[1-9]\)-[A-Z][a-z][a-z]-[1-9][0-9][0-9][0-9]'
|
|
||||||
|
|
||||||
syn keyword metamathTodo contained TODO FIXME Todo
|
|
||||||
|
|
||||||
syn match metamathDiscouraged contained
|
|
||||||
\ '\((Proof modification is discouraged.)\|(New usage is discouraged.)\)'
|
|
||||||
|
|
||||||
" External bibliography reference. See 'help write bibliography'
|
|
||||||
" in the metamath C program, which says:
|
|
||||||
" A name in square brackets in a statement's description (the comment before
|
|
||||||
" a $a or $p statement) indicates a bibliographic reference. The full
|
|
||||||
" reference must be of the form
|
|
||||||
" <keyword> <identifier> <noise word(s)> [<author>] p. <nnn>
|
|
||||||
" There should be no comma between '[<author>]' and 'p.'.
|
|
||||||
" Whitespace, comma, period, or semicolon should follow <nnn>.
|
|
||||||
" Example:
|
|
||||||
" Theorem 3.1 of [Monk] p. 22,
|
|
||||||
" The <keyword>, which is not case-sensitive,
|
|
||||||
" must be one of the following: Axiom, Chapter, Compare, Condition,
|
|
||||||
" Corollary, Definition, Equation, Example, Exercise, Figure, Item,
|
|
||||||
" Lemma, Lemmas, Line, Lines, Notation, Part, Postulate, Problem, Property,
|
|
||||||
" Proposition, Remark, Rule, Scheme, Section, Theorem.
|
|
||||||
" The <identifier> is optional, as in for example
|
|
||||||
" "Remark in [Monk] p. 22".
|
|
||||||
" The <noise word(s)> are zero or more from the list: from, in, of, on.
|
|
||||||
" These are ignored when
|
|
||||||
" generating the bibliographic cross-reference. The <author> must be present
|
|
||||||
" in the file identified with the htmlbibliography assignment (e.g.
|
|
||||||
" mmset.html) in the database $t comment, in the form <A NAME="<author>"></A>
|
|
||||||
" e.g. <A NAME="Monk"></A>. The <nnn> may be any alphanumeric string such as
|
|
||||||
" an integer or Roman numeral.
|
|
||||||
syn match metamathBibReference contained
|
|
||||||
\ '\c\(Axiom\|Chapter\|Compare\|Condition\|\|Corollary\|Definition\|Equation\|Example\|Exercise\|Figure\|Item\|Lemmas\?\|Lines\?\|Notation\|Part\|Postulate\|Problem\|Property\|Proposition\|Remark\|Rule\|Scheme\|Section\|Theorem\)[ \t\n\r]\+\([^\t\n\r]\{1,10\}[ \t\n\r]\+\)\?\(\(from\|in\|of\|on\)[ \t\n\r]\+\)\?\[[^ \t\n\r\[\]]*\][ \t\n\r]\+p\.[ \t\n\r]\+[^ \t\n\r]\+'
|
|
||||||
|
|
||||||
syn match metamathURL contained
|
|
||||||
\ '\<https\?://[^ \t]\+\>'
|
|
||||||
|
|
||||||
" Specially match long-standing bugs in the introductory set.mm comments
|
|
||||||
" (they're not as critical because it's never rendered).
|
|
||||||
syn match metamathSetMMBug contained
|
|
||||||
\ '\(changed \"D e\. Met\" to \"D e\. ( Met ` X )\",\|revised ( ( fLim ` J ) ` F ) -> ( J fLim F )\|is interpreted as a single ` \. A special\|\"( f ` x )\" should be read \"the value of function f at x\"\)'
|
|
||||||
|
|
||||||
" Highlight characters other than the officially
|
|
||||||
" legal characters (per spec), which are A-Z, a-z, 0-9, and:
|
|
||||||
" ` ~ ! @ # $ % ^ & * ( ) - _ = +
|
|
||||||
" [ ] { } ; : ' " , . < > / ? \ |
|
|
||||||
syn match metamathIllegalChar contained
|
|
||||||
\ '[^A-Za-z0-9`~!@#$%^&*()_=+\[\]{};:'\",.<>/?\\| \t\n\r\f-]'
|
|
||||||
|
|
||||||
" Some text within a comment is special; this cluster lists them.
|
|
||||||
syn cluster metamathSpecialComment
|
|
||||||
\ contains=metamathXref,metamathEmbeddedExpression,metamathDate,metamathTodo,metamathDiscouraged,metamathBibReference,metamathURL,metamathSetMMBug,metamathIllegalChar
|
|
||||||
|
|
||||||
|
|
||||||
" metamathComments do NOT nest, so we use keepend.
|
|
||||||
syn region metamathComment
|
|
||||||
\ start='\<$(\>'
|
|
||||||
\ end='\<$)\>'
|
|
||||||
\ contains=metamathTrailingSpace,@metamathSpecialComment,@Spell
|
|
||||||
" \ conceal keepend
|
|
||||||
|
|
||||||
" $c ... $. - Constant declaration
|
|
||||||
syn region metamathConstant
|
|
||||||
\ start='\<$c\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
|
|
||||||
" $v ... $. - Variable declaration
|
|
||||||
syn region metamathVariable
|
|
||||||
\ start='\<$v\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
|
|
||||||
" $d ... $. - Disjoint (distinct) variable restriction
|
|
||||||
syn region metamathDisjoint
|
|
||||||
\ start='\<$d\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
|
|
||||||
" The following constructs require labels, so require that the label
|
|
||||||
" be processed first.
|
|
||||||
|
|
||||||
" <label> $f ... $. - "Floating" hypothesis (i.e. variable type declaration)
|
|
||||||
syn region metamathFloating contained
|
|
||||||
\ start='\<$f\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
|
|
||||||
" <label> $e ... $. - "Essential" hypothesis (i.e. a logical assumption for a
|
|
||||||
" theorem or axiom)
|
|
||||||
syn region metamathEssential contained
|
|
||||||
\ start='\<$e\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
\ contains=@metamathExpression
|
|
||||||
|
|
||||||
" <label> $a ... $. - Axiom or definition or syntax construction
|
|
||||||
syn region metamathAxiom contained
|
|
||||||
\ start='\<$a\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
\ contains=@metamathExpression
|
|
||||||
|
|
||||||
" <label> $p ... $= ... $. - Theorem and its proof.
|
|
||||||
" This handles the first part before "$="; on "$=" we start "metamathProof",
|
|
||||||
" which looks different. The "keepend" is needed to end with metamathProof.
|
|
||||||
syn region metamathTheorem contained
|
|
||||||
\ start='\<$p\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
\ contains=metamathProof,@metamathExpression
|
|
||||||
\ keepend
|
|
||||||
|
|
||||||
" This is the proof part of a theorem.
|
|
||||||
syn region metamathProof contained
|
|
||||||
\ start='\<$=\>'
|
|
||||||
\ end='\<$\.\>'
|
|
||||||
\ contains=metamathTrailingSpace
|
|
||||||
|
|
||||||
" $[ ... $] - Include a file
|
|
||||||
syn region metamathInclude
|
|
||||||
\ start='\<$\[\>'
|
|
||||||
\ end='\<$\]\>'
|
|
||||||
|
|
||||||
" ${ ... $} - Block
|
|
||||||
syn region metamathBlock
|
|
||||||
\ start='${'
|
|
||||||
\ end='$}'
|
|
||||||
\ contains=TOP
|
|
||||||
\ transparent
|
|
||||||
|
|
||||||
" Highlight lables, and then handle labelled constructs (but only when
|
|
||||||
" the required label is there).
|
|
||||||
syn cluster metamathLabelled
|
|
||||||
\ contains=metamathFloating,metamathEssential,metamathAxiom,metamathTheorem,metamathProof
|
|
||||||
|
|
||||||
syn match metamathLabel '\<[A-Za-z0-9_.-]\+\>'
|
|
||||||
\ nextgroup=@metamathLabelled
|
|
||||||
\ skipwhite skipempty
|
|
||||||
|
|
||||||
" Trailing space is bad for version control - warn about it.
|
|
||||||
syn match metamathTrailingSpace '[ \t]\+$'
|
|
||||||
|
|
||||||
" Technically metamath doesn't "know" about specific constants in
|
|
||||||
" math expressions. Even parentheses must be defined.
|
|
||||||
" However, typical metamath files define some specific common constructs
|
|
||||||
" constants as numbers, parentheses, turnstile,
|
|
||||||
" fundamental logical operators, and so on.
|
|
||||||
" They are unlikely to have unexpected meanings.
|
|
||||||
" So let's recognize them, emphasizing those very low-level constructs.
|
|
||||||
" This provides some contrast with other parts of an expression,
|
|
||||||
" and the visual contrast can help the eye notice a defect.
|
|
||||||
" If you don't want to recognize these, set "metamath_omit_common".
|
|
||||||
if !exists('g:metamath_omit_common')
|
|
||||||
syn match metamathNumber contained '\<\d\+\>'
|
|
||||||
syn keyword metamathBoolean contained T.
|
|
||||||
syn keyword metamathBoolean contained F.
|
|
||||||
syn keyword metamathBasicOperator contained \|-
|
|
||||||
syn keyword metamathBasicOperator contained ->
|
|
||||||
syn keyword metamathBasicOperator contained <->
|
|
||||||
syn keyword metamathBasicOperator contained -.
|
|
||||||
syn keyword metamathBasicOperator contained (
|
|
||||||
syn keyword metamathBasicOperator contained )
|
|
||||||
syn keyword metamathBasicOperator contained \\/
|
|
||||||
syn keyword metamathBasicOperator contained /\
|
|
||||||
syn keyword metamathBasicOperator contained A.
|
|
||||||
syn keyword metamathBasicOperator contained E.
|
|
||||||
syn keyword metamathBasicOperator contained e.
|
|
||||||
syn keyword metamathBasicOperator contained =
|
|
||||||
endif
|
|
||||||
|
|
||||||
syn cluster metamathExpression
|
|
||||||
\ contains=metamathNumber,metamathBoolean,metamathBasicOperator,metamathTrailingSpace
|
|
||||||
|
|
||||||
let b:current_syntax = 'metamath'
|
|
||||||
|
|
||||||
" Define highlighting. The "standard" names don't map well
|
|
||||||
" to metamath constructs; this mapping probably needs work.
|
|
||||||
" For list see http://vimdoc.sourceforge.net/htmldoc/syntax.html#:highlight
|
|
||||||
highlight def link metamathBadStatement Error
|
|
||||||
highlight def link metamathComment Comment
|
|
||||||
highlight def link metamathXref Underlined
|
|
||||||
highlight def link metamathURL Underlined
|
|
||||||
highlight def link metamathDate SpecialComment
|
|
||||||
highlight def link metamathDiscouraged SpecialComment
|
|
||||||
highlight def link metamathEmbeddedExpression Structure " metamathTheorem
|
|
||||||
highlight def link metamathBibReference SpecialComment
|
|
||||||
highlight def link metamathSetMMBug Error
|
|
||||||
highlight def link metamathIllegalChar Error
|
|
||||||
highlight def link metamathTodo Todo
|
|
||||||
|
|
||||||
highlight def link metamathConstant Constant
|
|
||||||
highlight def link metamathVariable Constant
|
|
||||||
highlight def link metamathDisjoint Statement
|
|
||||||
highlight def link metamathFloating Statement
|
|
||||||
highlight def link metamathEssential Statement
|
|
||||||
highlight def link metamathAxiom Statement
|
|
||||||
highlight def link metamathTheorem Structure
|
|
||||||
highlight def link metamathProof Define
|
|
||||||
highlight def link metamathInclude Include
|
|
||||||
highlight def link metamathTrailingSpace Error
|
|
||||||
highlight def link metamathLabel Label
|
|
||||||
|
|
||||||
highlight def link metamathBoolean Boolean
|
|
||||||
highlight def link metamathNumber Number
|
|
||||||
highlight def link metamathBasicOperator Constant
|
|
||||||
|
|
||||||
Loading…
Reference in a new issue