From 44625f1ccf03a750526b3665caf3e2485580c363 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sun, 6 Oct 2024 16:40:37 -0700 Subject: [PATCH] completely rewrote neovim config --- nvim/.config/nvim/after/ftplugin/haskell.lua | 1 + nvim/.config/nvim/ftdetect/metamath.vim | 2 - nvim/.config/nvim/init.lua | 6 +- nvim/.config/nvim/lua/keymaps.lua | 9 + nvim/.config/nvim/lua/lazy_init.lua | 23 ++ .../nvim/lua/{wball/core => }/options.lua | 10 +- nvim/.config/nvim/lua/plugins/colors.lua | 10 + nvim/.config/nvim/lua/plugins/completion.lua | 55 ++++ nvim/.config/nvim/lua/plugins/init.lua | 3 + nvim/.config/nvim/lua/plugins/keys.lua | 23 ++ .../nvim/lua/plugins/languages/coq.lua | 16 ++ .../nvim/lua/plugins/languages/haskell.lua | 7 + .../nvim/lua/plugins/languages/init.lua | 1 + .../plugins => plugins/languages}/lean.lua | 0 .../nvim/lua/plugins/languages/rust.lua | 7 + nvim/.config/nvim/lua/plugins/lsp.lua | 49 ++++ nvim/.config/nvim/lua/plugins/telescope.lua | 81 ++++++ nvim/.config/nvim/lua/plugins/treesitter.lua | 18 ++ nvim/.config/nvim/lua/plugins/ui.lua | 6 + nvim/.config/nvim/lua/plugins/utils.lua | 51 ++++ nvim/.config/nvim/lua/wball/core/keymaps.lua | 26 -- nvim/.config/nvim/lua/wball/lazy.lua | 25 -- .../nvim/lua/wball/plugins/autopairs.lua | 24 -- .../nvim/lua/wball/plugins/colorscheme.lua | 22 -- .../nvim/lua/wball/plugins/comment.lua | 12 - .../nvim/lua/wball/plugins/conform.lua | 16 -- .../nvim/lua/wball/plugins/dressing.lua | 4 - nvim/.config/nvim/lua/wball/plugins/init.lua | 3 - .../nvim/lua/wball/plugins/isabelle.lua | 18 -- .../nvim/lua/wball/plugins/languages.lua | 11 - .../nvim/lua/wball/plugins/lsp/coq.lua | 8 - .../nvim/lua/wball/plugins/lsp/haskell.lua | 5 - .../nvim/lua/wball/plugins/lsp/lspconfig.lua | 75 ------ .../nvim/lua/wball/plugins/lsp/miscutils.lua | 6 - .../nvim/lua/wball/plugins/lsp/rust.lua | 4 - .../.config/nvim/lua/wball/plugins/neogit.lua | 22 -- .../nvim/lua/wball/plugins/nvim-cmp.lua | 57 ----- .../nvim/lua/wball/plugins/nvim-tree.lua | 17 -- nvim/.config/nvim/lua/wball/plugins/sml.lua | 5 - .../nvim/lua/wball/plugins/surround.lua | 6 - .../nvim/lua/wball/plugins/telescope.lua | 36 --- .../nvim/lua/wball/plugins/terminal.lua | 12 - nvim/.config/nvim/lua/wball/plugins/tmux.lua | 11 - .../nvim/lua/wball/plugins/todo-comments.lua | 18 -- .../nvim/lua/wball/plugins/treesitter.lua | 30 --- nvim/.config/nvim/lua/wball/plugins/vifm.lua | 3 - .../nvim/lua/wball/plugins/which-key.lua | 9 - nvim/.config/nvim/syntax/metamath.vim | 240 ------------------ 48 files changed, 367 insertions(+), 736 deletions(-) create mode 100644 nvim/.config/nvim/after/ftplugin/haskell.lua delete mode 100644 nvim/.config/nvim/ftdetect/metamath.vim create mode 100644 nvim/.config/nvim/lua/keymaps.lua create mode 100644 nvim/.config/nvim/lua/lazy_init.lua rename nvim/.config/nvim/lua/{wball/core => }/options.lua (74%) create mode 100644 nvim/.config/nvim/lua/plugins/colors.lua create mode 100644 nvim/.config/nvim/lua/plugins/completion.lua create mode 100644 nvim/.config/nvim/lua/plugins/init.lua create mode 100644 nvim/.config/nvim/lua/plugins/keys.lua create mode 100644 nvim/.config/nvim/lua/plugins/languages/coq.lua create mode 100644 nvim/.config/nvim/lua/plugins/languages/haskell.lua create mode 100644 nvim/.config/nvim/lua/plugins/languages/init.lua rename nvim/.config/nvim/lua/{wball/plugins => plugins/languages}/lean.lua (100%) create mode 100644 nvim/.config/nvim/lua/plugins/languages/rust.lua create mode 100644 nvim/.config/nvim/lua/plugins/lsp.lua create mode 100644 nvim/.config/nvim/lua/plugins/telescope.lua create mode 100644 nvim/.config/nvim/lua/plugins/treesitter.lua create mode 100644 nvim/.config/nvim/lua/plugins/ui.lua create mode 100644 nvim/.config/nvim/lua/plugins/utils.lua delete mode 100644 nvim/.config/nvim/lua/wball/core/keymaps.lua delete mode 100644 nvim/.config/nvim/lua/wball/lazy.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/autopairs.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/colorscheme.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/comment.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/conform.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/dressing.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/init.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/isabelle.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/languages.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/lsp/coq.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/lsp/haskell.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/lsp/lspconfig.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/lsp/miscutils.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/lsp/rust.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/neogit.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/nvim-cmp.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/nvim-tree.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/sml.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/surround.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/telescope.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/terminal.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/tmux.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/todo-comments.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/treesitter.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/vifm.lua delete mode 100644 nvim/.config/nvim/lua/wball/plugins/which-key.lua delete mode 100644 nvim/.config/nvim/syntax/metamath.vim diff --git a/nvim/.config/nvim/after/ftplugin/haskell.lua b/nvim/.config/nvim/after/ftplugin/haskell.lua new file mode 100644 index 0000000..4ce8999 --- /dev/null +++ b/nvim/.config/nvim/after/ftplugin/haskell.lua @@ -0,0 +1 @@ +require('haskell-tools').lsp.start() diff --git a/nvim/.config/nvim/ftdetect/metamath.vim b/nvim/.config/nvim/ftdetect/metamath.vim deleted file mode 100644 index 48d2f6d..0000000 --- a/nvim/.config/nvim/ftdetect/metamath.vim +++ /dev/null @@ -1,2 +0,0 @@ -au BufRead,BufNewFile *.mm set filetype=metamath -au BufRead,BufNewFile *.mma set filetype=metamath diff --git a/nvim/.config/nvim/init.lua b/nvim/.config/nvim/init.lua index c54f6fd..5187213 100644 --- a/nvim/.config/nvim/init.lua +++ b/nvim/.config/nvim/init.lua @@ -1,4 +1,4 @@ -require("wball.core.options") -require("wball.core.keymaps") +require('options') +require('keymaps') -require("wball.lazy") +require('lazy_init') diff --git a/nvim/.config/nvim/lua/keymaps.lua b/nvim/.config/nvim/lua/keymaps.lua new file mode 100644 index 0000000..05a5eca --- /dev/null +++ b/nvim/.config/nvim/lua/keymaps.lua @@ -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') diff --git a/nvim/.config/nvim/lua/lazy_init.lua b/nvim/.config/nvim/lua/lazy_init.lua new file mode 100644 index 0000000..94e143b --- /dev/null +++ b/nvim/.config/nvim/lua/lazy_init.lua @@ -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 }, +}) diff --git a/nvim/.config/nvim/lua/wball/core/options.lua b/nvim/.config/nvim/lua/options.lua similarity index 74% rename from nvim/.config/nvim/lua/wball/core/options.lua rename to nvim/.config/nvim/lua/options.lua index 81cbfb0..c035d93 100644 --- a/nvim/.config/nvim/lua/wball/core/options.lua +++ b/nvim/.config/nvim/lua/options.lua @@ -13,20 +13,18 @@ opt.autoindent = true opt.ignorecase = true opt.smartcase = true -opt.cursorline = true - opt.termguicolors = true -opt.signcolumn = "yes" +opt.signcolumn = 'yes' -opt.clipboard:append("unnamedplus") +opt.clipboard:append('unnamedplus') opt.conceallevel = 2 opt.breakindent = true opt.linebreak = true -vim.api.nvim_create_autocmd("TermOpen", { - pattern = "*", +vim.api.nvim_create_autocmd('TermOpen', { + pattern = '*', callback = function() vim.opt.number = false vim.opt.relativenumber = false diff --git a/nvim/.config/nvim/lua/plugins/colors.lua b/nvim/.config/nvim/lua/plugins/colors.lua new file mode 100644 index 0000000..83b90c8 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/colors.lua @@ -0,0 +1,10 @@ +return { + { + 'catppuccin/nvim', + name = 'catppuccin', + priority = 1000, + config = function() + vim.cmd.colorscheme([[catppuccin-mocha]]) + end + } +} diff --git a/nvim/.config/nvim/lua/plugins/completion.lua b/nvim/.config/nvim/lua/plugins/completion.lua new file mode 100644 index 0000000..017a5d4 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/completion.lua @@ -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({ + [''] = cmp.mapping.scroll_docs(-4), + [''] = cmp.mapping.scroll_docs(4), + [''] = cmp.mapping.complete(), + [''] = cmp.mapping.abort(), + [''] = 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 + } +} diff --git a/nvim/.config/nvim/lua/plugins/init.lua b/nvim/.config/nvim/lua/plugins/init.lua new file mode 100644 index 0000000..89e9a69 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/init.lua @@ -0,0 +1,3 @@ +return { + 'nvim-lua/plenary.nvim' +} diff --git a/nvim/.config/nvim/lua/plugins/keys.lua b/nvim/.config/nvim/lua/plugins/keys.lua new file mode 100644 index 0000000..e8c68e0 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/keys.lua @@ -0,0 +1,23 @@ +return { + { + 'folke/which-key.nvim', + event = 'VeryLazy', + config = function() + -- set up groups + local wk = require('which-key') + wk.add({ + { 'f', group = 'find' }, + { 'h', group = 'help' }, + }) + end, + keys = { + { + "?", + function() + require("which-key").show({ global = false }) + end, + desc = "Buffer Local Keymaps (which-key)", + }, + }, + } +} diff --git a/nvim/.config/nvim/lua/plugins/languages/coq.lua b/nvim/.config/nvim/lua/plugins/languages/coq.lua new file mode 100644 index 0000000..0f3d74d --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/languages/coq.lua @@ -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' } + } +} diff --git a/nvim/.config/nvim/lua/plugins/languages/haskell.lua b/nvim/.config/nvim/lua/plugins/languages/haskell.lua new file mode 100644 index 0000000..f48044d --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/languages/haskell.lua @@ -0,0 +1,7 @@ +return { + { + 'mrcjkb/haskell-tools.nvim', + version = '^4', + lazy = false, + } +} diff --git a/nvim/.config/nvim/lua/plugins/languages/init.lua b/nvim/.config/nvim/lua/plugins/languages/init.lua new file mode 100644 index 0000000..a564707 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/languages/init.lua @@ -0,0 +1 @@ +return {} diff --git a/nvim/.config/nvim/lua/wball/plugins/lean.lua b/nvim/.config/nvim/lua/plugins/languages/lean.lua similarity index 100% rename from nvim/.config/nvim/lua/wball/plugins/lean.lua rename to nvim/.config/nvim/lua/plugins/languages/lean.lua diff --git a/nvim/.config/nvim/lua/plugins/languages/rust.lua b/nvim/.config/nvim/lua/plugins/languages/rust.lua new file mode 100644 index 0000000..25fed50 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/languages/rust.lua @@ -0,0 +1,7 @@ +return { + { + 'mrcjkb/rustaceanvim', + version = '^5', + lazy = false + } +} diff --git a/nvim/.config/nvim/lua/plugins/lsp.lua b/nvim/.config/nvim/lua/plugins/lsp.lua new file mode 100644 index 0000000..7f87cd0 --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/lsp.lua @@ -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' }, + + { 'la', vim.lsp.buf.code_action, desc = 'See available code actions' }, + { 'lr', vim.lsp.buf.rename, desc = 'Rename' }, + { 'lf', vim.lsp.buf.format, desc = 'Format' }, + { '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' + } +} diff --git a/nvim/.config/nvim/lua/plugins/telescope.lua b/nvim/.config/nvim/lua/plugins/telescope.lua new file mode 100644 index 0000000..0f8253b --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/telescope.lua @@ -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 = { + { + "ff", + require('telescope.builtin').find_files, + desc = 'Telescope find files' + }, + { + "fg", + require('telescope.builtin').live_grep, + desc = 'Telescope live grep' + }, + { + "fb", + require('telescope.builtin').buffers, + desc = 'Telescope buffers' + }, + { + "fh", + require('telescope.builtin').help_tags, + desc = 'Telescope help tags' + }, + { + "fo", + require('telescope.builtin').oldfiles, + desc = 'Telescope old files' + }, + { + "fc", + require('telescope.builtin').commands, + desc = 'Telescope commands' + }, + { + "fm", + require('telescope.builtin').marks, + desc = 'Telescope marks' + }, + { + "fq", + require('telescope.builtin').quickfix, + desc = 'Telescope quickfix' + }, + { + "fl", + require('telescope.builtin').loclist, + desc = 'Telescope loclist' + }, + { + "fr", + require('telescope.builtin').registers, + desc = 'Telescope registers' + }, + } + }, + { + 'nvim-telescope/telescope-fzf-native.nvim', + build = 'make' + } +} diff --git a/nvim/.config/nvim/lua/plugins/treesitter.lua b/nvim/.config/nvim/lua/plugins/treesitter.lua new file mode 100644 index 0000000..47b022f --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/treesitter.lua @@ -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' + } +} diff --git a/nvim/.config/nvim/lua/plugins/ui.lua b/nvim/.config/nvim/lua/plugins/ui.lua new file mode 100644 index 0000000..636052c --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/ui.lua @@ -0,0 +1,6 @@ +return { + { + 'stevearc/dressing.nvim', + opts = {}, + } +} diff --git a/nvim/.config/nvim/lua/plugins/utils.lua b/nvim/.config/nvim/lua/plugins/utils.lua new file mode 100644 index 0000000..4a2e22f --- /dev/null +++ b/nvim/.config/nvim/lua/plugins/utils.lua @@ -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({ + { 'g', group = 'git' }, + { 'gn', neogit.open, desc = 'Neogit' }, + { 'gd', ':DiffviewOpen', 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 + } +} diff --git a/nvim/.config/nvim/lua/wball/core/keymaps.lua b/nvim/.config/nvim/lua/wball/core/keymaps.lua deleted file mode 100644 index 5accc5f..0000000 --- a/nvim/.config/nvim/lua/wball/core/keymaps.lua +++ /dev/null @@ -1,26 +0,0 @@ -local keymap = vim.keymap - --- set leader key to space -vim.g.mapleader = ' ' -vim.g.maplocalleader = ' ' - --- let move around windows --- keymap.set('n', '', 'h') --- keymap.set('n', '', 'j') --- keymap.set('n', '', 'k') --- keymap.set('n', '', 'l') - --- same with terminals --- keymap.set('t', '', 'h') --- keymap.set('t', '', 'j') --- keymap.set('t', '', 'k') --- keymap.set('t', '', '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", "nh", ":nohl", { desc = "Clear highlight" }) diff --git a/nvim/.config/nvim/lua/wball/lazy.lua b/nvim/.config/nvim/lua/wball/lazy.lua deleted file mode 100644 index de7be51..0000000 --- a/nvim/.config/nvim/lua/wball/lazy.lua +++ /dev/null @@ -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, - }, -}) diff --git a/nvim/.config/nvim/lua/wball/plugins/autopairs.lua b/nvim/.config/nvim/lua/wball/plugins/autopairs.lua deleted file mode 100644 index ab34429..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/autopairs.lua +++ /dev/null @@ -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 -} diff --git a/nvim/.config/nvim/lua/wball/plugins/colorscheme.lua b/nvim/.config/nvim/lua/wball/plugins/colorscheme.lua deleted file mode 100644 index 8b99653..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/colorscheme.lua +++ /dev/null @@ -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 - } -} diff --git a/nvim/.config/nvim/lua/wball/plugins/comment.lua b/nvim/.config/nvim/lua/wball/plugins/comment.lua deleted file mode 100644 index c7d56e2..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/comment.lua +++ /dev/null @@ -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 -} diff --git a/nvim/.config/nvim/lua/wball/plugins/conform.lua b/nvim/.config/nvim/lua/wball/plugins/conform.lua deleted file mode 100644 index 2f5ba95..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/conform.lua +++ /dev/null @@ -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", - }, - } - } -} diff --git a/nvim/.config/nvim/lua/wball/plugins/dressing.lua b/nvim/.config/nvim/lua/wball/plugins/dressing.lua deleted file mode 100644 index 32df64b..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/dressing.lua +++ /dev/null @@ -1,4 +0,0 @@ -return { - "stevearc/dressing.nvim", - event = "VeryLazy", -} diff --git a/nvim/.config/nvim/lua/wball/plugins/init.lua b/nvim/.config/nvim/lua/wball/plugins/init.lua deleted file mode 100644 index d2c1874..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/init.lua +++ /dev/null @@ -1,3 +0,0 @@ -return { - "nvim-lua/plenary.nvim" -} diff --git a/nvim/.config/nvim/lua/wball/plugins/isabelle.lua b/nvim/.config/nvim/lua/wball/plugins/isabelle.lua deleted file mode 100644 index a24d9f6..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/isabelle.lua +++ /dev/null @@ -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 - } -} diff --git a/nvim/.config/nvim/lua/wball/plugins/languages.lua b/nvim/.config/nvim/lua/wball/plugins/languages.lua deleted file mode 100644 index 0e9b417..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/languages.lua +++ /dev/null @@ -1,11 +0,0 @@ -return { - { - "whonore/Coqtail" - }, - { - "https://git.sr.ht/~sircmpwn/hare.vim" - }, - { - "https://git.sr.ht/~torresjrjr/vim-haredoc" - }, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/lsp/coq.lua b/nvim/.config/nvim/lua/wball/plugins/lsp/coq.lua deleted file mode 100644 index e23a53f..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/lsp/coq.lua +++ /dev/null @@ -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 -} diff --git a/nvim/.config/nvim/lua/wball/plugins/lsp/haskell.lua b/nvim/.config/nvim/lua/wball/plugins/lsp/haskell.lua deleted file mode 100644 index 21e0245..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/lsp/haskell.lua +++ /dev/null @@ -1,5 +0,0 @@ -return { - 'mrcjkb/haskell-tools.nvim', - version = '^3', - ft = { 'haskell', 'lhaskell', 'cabal', 'cabalproject' }, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/lsp/lspconfig.lua b/nvim/.config/nvim/lua/wball/plugins/lsp/lspconfig.lua deleted file mode 100644 index 19cbd5d..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/lsp/lspconfig.lua +++ /dev/null @@ -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", "Telescope lsp_references", opts) - - opts.desc = "Go to declaration" - keymap.set("n", "gD", vim.lsp.buf.declaration, opts) - - opts.desc = "Show LSP definitions" - keymap.set("n", "gd", "Telescope lsp_definitions", opts) - - opts.desc = "Show LSP implementations" - keymap.set("n", "gi", "Telescope lsp_implementations", opts) - - opts.desc = "Show LSP type definitions" - keymap.set("n", "gt", "Telescope lsp_type_definitions", opts) - - opts.desc = "See available code actions" - keymap.set({ "n", "v" }, "la", vim.lsp.buf.code_action, opts) - - opts.desc = "Smart rename" - keymap.set("n", "lr", vim.lsp.buf.rename, opts) - - opts.desc = "Format" - keymap.set("n", "lf", vim.lsp.buf.format, opts) - - opts.desc = "Show buffer diagnostics" - keymap.set("n", "ld", "Telescope diagnostics bufnr=0", opts) - - opts.desc = "Show line diagnostics" - keymap.set("n", "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", "ls", ":LspRestart", opts) - end, - }) - - vim.lsp.handlers['textDocument/hover'] = vim.lsp.with(vim.lsp.handlers.hover, { border = "single" }) - - vim.diagnostic.config({ virtual_text = true }) - end, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/lsp/miscutils.lua b/nvim/.config/nvim/lua/wball/plugins/lsp/miscutils.lua deleted file mode 100644 index 6c4cf77..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/lsp/miscutils.lua +++ /dev/null @@ -1,6 +0,0 @@ -return { - { - "j-hui/fidget.nvim", - config = true, - }, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/lsp/rust.lua b/nvim/.config/nvim/lua/wball/plugins/lsp/rust.lua deleted file mode 100644 index 1837ea6..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/lsp/rust.lua +++ /dev/null @@ -1,4 +0,0 @@ -return { - 'vxpm/ferris.nvim', - config = true, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/neogit.lua b/nvim/.config/nvim/lua/wball/plugins/neogit.lua deleted file mode 100644 index 19b7045..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/neogit.lua +++ /dev/null @@ -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", - "go", - function() - neogit.open({ kind="auto" }) - end, - { desc = "Open Neogit in new split" }) - vim.keymap.set("n", "gg", neogit.open, { desc = "Open Neogit in new tab "}) - - neogit.setup() - end - } -} diff --git a/nvim/.config/nvim/lua/wball/plugins/nvim-cmp.lua b/nvim/.config/nvim/lua/wball/plugins/nvim-cmp.lua deleted file mode 100644 index 7ea2efd..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/nvim-cmp.lua +++ /dev/null @@ -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({ - [""] = cmp.mapping.select_prev_item(), - [""] = cmp.mapping.select_next_item(), - [""] = cmp.mapping.scroll_docs(-4), - [""] = cmp.mapping.scroll_docs(4), - [""] = cmp.mapping.complete(), - [""] = cmp.mapping.abort(), - [""] = 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, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/nvim-tree.lua b/nvim/.config/nvim/lua/wball/plugins/nvim-tree.lua deleted file mode 100644 index 907dc47..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/nvim-tree.lua +++ /dev/null @@ -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", "ee", "NvimTreeToggle", { desc = "Toggle NvimTree" }) - vim.keymap.set("n", "ef", "NvimTreeFindFileToggle", { desc = "Toggle NvimTree on current file" }) - vim.keymap.set("n", "ec", "NvimTreeCollapse", { desc = "Collapse NvimTree" }) - vim.keymap.set("n", "er", "NvimTreeRefresh", { desc = "Refresh NvimTree" }) - end -} diff --git a/nvim/.config/nvim/lua/wball/plugins/sml.lua b/nvim/.config/nvim/lua/wball/plugins/sml.lua deleted file mode 100644 index 3fb70be..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/sml.lua +++ /dev/null @@ -1,5 +0,0 @@ -return { - { - 'jez/vim-better-sml' - } -} diff --git a/nvim/.config/nvim/lua/wball/plugins/surround.lua b/nvim/.config/nvim/lua/wball/plugins/surround.lua deleted file mode 100644 index 153dec8..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/surround.lua +++ /dev/null @@ -1,6 +0,0 @@ -return { - "kylechui/nvim-surround", - event = { "BufReadPre", "BufNewFile" }, - version = "*", - config = true, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/telescope.lua b/nvim/.config/nvim/lua/wball/plugins/telescope.lua deleted file mode 100644 index b60cae5..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/telescope.lua +++ /dev/null @@ -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", "ff", builtin.find_files, { desc = "Fuzzy find files in cwd" }) - vim.keymap.set("n", "fr", builtin.registers, { desc = "Fuzzy find registers" }) - vim.keymap.set("n", "fb", builtin.buffers, { desc = "Fuzzy find buffers" }) - vim.keymap.set("n", "fl", builtin.live_grep, { desc = "Live grep" }) - vim.keymap.set("n", "fs", builtin.grep_string, { desc = "Grep string under cursor in cwd" }) - vim.keymap.set("n", "ftt", builtin.tags, { desc = "Fuzzy find tags" }) - vim.keymap.set("n", "fgf", builtin.git_files, { desc = "Fuzzy search git files" }) - vim.keymap.set("n", "fgc", builtin.git_commits, { desc = "Fuzzy search git commits" }) - vim.keymap.set("n", "ftb", builtin.builtin, { desc = "Search telescope builtins" }) - vim.keymap.set("n", "fc", builtin.commands, { desc = "Fuzzy search commands" }) - vim.keymap.set("n", "fq", builtin.quickfix, { desc = "Search quickfix list" }) - vim.keymap.set("n", "fl", builtin.loclist, { desc = "Search loclist" }) - vim.keymap.set("n", "fh", builtin.help_tags, { desc = "Search help tags" }) - vim.keymap.set("n", "fm", builtin.marks, { desc = "Search marks" }) - vim.keymap.set("n", "fd", "TodoTelescope", { desc = "Find todos" }) - end -} diff --git a/nvim/.config/nvim/lua/wball/plugins/terminal.lua b/nvim/.config/nvim/lua/wball/plugins/terminal.lua deleted file mode 100644 index 7de717f..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/terminal.lua +++ /dev/null @@ -1,12 +0,0 @@ -return { - { - "akinsho/toggleterm.nvim", - opts = { - open_mapping = [[]], - direction = "horizontal", - insert_mappings = true, - start_in_insert = true, - }, - keys = [[]], - }, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/tmux.lua b/nvim/.config/nvim/lua/wball/plugins/tmux.lua deleted file mode 100644 index 77a244c..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/tmux.lua +++ /dev/null @@ -1,11 +0,0 @@ -return { - "numToStr/Navigator.nvim", - config = function() - require('Navigator').setup() - vim.keymap.set({'n', 't'}, '', 'NavigatorLeft') - vim.keymap.set({'n', 't'}, '', 'NavigatorRight') - vim.keymap.set({'n', 't'}, '', 'NavigatorUp') - vim.keymap.set({'n', 't'}, '', 'NavigatorDown') - vim.keymap.set({'n', 't'}, '', 'NavigatorPrevious') - end, -} diff --git a/nvim/.config/nvim/lua/wball/plugins/todo-comments.lua b/nvim/.config/nvim/lua/wball/plugins/todo-comments.lua deleted file mode 100644 index 6bdf756..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/todo-comments.lua +++ /dev/null @@ -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 -} diff --git a/nvim/.config/nvim/lua/wball/plugins/treesitter.lua b/nvim/.config/nvim/lua/wball/plugins/treesitter.lua deleted file mode 100644 index e3286cc..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/treesitter.lua +++ /dev/null @@ -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 = "", - node_incremental = "", - scope_incremental = false, - node_decremental = "", - } - } - }) - end -} diff --git a/nvim/.config/nvim/lua/wball/plugins/vifm.lua b/nvim/.config/nvim/lua/wball/plugins/vifm.lua deleted file mode 100644 index becc05f..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/vifm.lua +++ /dev/null @@ -1,3 +0,0 @@ -return { - "vifm/vifm.vim", -} diff --git a/nvim/.config/nvim/lua/wball/plugins/which-key.lua b/nvim/.config/nvim/lua/wball/plugins/which-key.lua deleted file mode 100644 index 5c94080..0000000 --- a/nvim/.config/nvim/lua/wball/plugins/which-key.lua +++ /dev/null @@ -1,9 +0,0 @@ -return { - "folke/which-key.nvim", - event = "VeryLazy", - init = function() - vim.o.timeout = true - vim.o.timeoutlen = 500 - end, - opts = {} -} diff --git a/nvim/.config/nvim/syntax/metamath.vim b/nvim/.config/nvim/syntax/metamath.vim deleted file mode 100644 index bbcafa3..0000000 --- a/nvim/.config/nvim/syntax/metamath.vim +++ /dev/null @@ -1,240 +0,0 @@ -" Vim syntax file -" Language: Metamath -" Maintainer: David A. Wheeler -" 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 -" [] p. -" There should be no comma between '[]' and 'p.'. -" Whitespace, comma, period, or semicolon should follow . -" Example: -" Theorem 3.1 of [Monk] p. 22, -" The , 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 is optional, as in for example -" "Remark in [Monk] p. 22". -" The are zero or more from the list: from, in, of, on. -" These are ignored when -" generating the bibliographic cross-reference. The must be present -" in the file identified with the htmlbibliography assignment (e.g. -" mmset.html) in the database $t comment, in the form -" e.g. . The 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 - \ '\' - -" 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. - -"