completely rewrote neovim config

fish/.config/fish/conf.d/rustup.fish

@@ -1 +1,2 @@
 . "/home/wball/.local/share/cargo/env.fish"
+source "/home/wball/.local/share/cargo/env.fish"

fish/.config/fish/config.fish

@@ -67,12 +67,3 @@ end
 eval (opam env --switch=default)
 
 set -q GHCUP_INSTALL_BASE_PREFIX[1]; or set GHCUP_INSTALL_BASE_PREFIX $HOME ; set -gx PATH $HOME/.cabal/bin $PATH /home/wball/.local/bin # ghcup-env
-
-# >>> JVM installed by coursier >>>
-set -gx JAVA_HOME "/home/wball/.cache/coursier/arc/https/github.com/adoptium/temurin11-binaries/releases/download/jdk-11.0.24%252B8/OpenJDK11U-jdk_x64_linux_hotspot_11.0.24_8.tar.gz/jdk-11.0.24+8"
-set -gx PATH "$PATH:/home/wball/.cache/coursier/arc/https/github.com/adoptium/temurin11-binaries/releases/download/jdk-11.0.24%252B8/OpenJDK11U-jdk_x64_linux_hotspot_11.0.24_8.tar.gz/jdk-11.0.24+8/bin"
-# <<< JVM installed by coursier <<<
-
-# >>> coursier install directory >>>
-set -gx PATH "$PATH:/home/wball/.local/share/coursier/bin"
-# <<< coursier install directory <<<

fish/.config/fish/fish_plugins

@@ -1,4 +1,3 @@
 jorgebucaran/fisher
 jethrokuan/z
 patrickf1/fzf.fish
-catppuccin/fish

fish/.config/fish/fish_variables

@@ -7,48 +7,48 @@ SETUVAR Z_DATA:/home/wball/\x2elocal/share/z/data
 SETUVAR Z_DATA_DIR:/home/wball/\x2elocal/share/z
 SETUVAR Z_EXCLUDE:\x5e/home/wball\x24
 SETUVAR __fish_initialized:3400
-SETUVAR _fisher_catppuccin_2F_fish_files:\x7e/\x2econfig/fish/themes/Catppuccin\x20Frappe\x2etheme\x1e\x7e/\x2econfig/fish/themes/Catppuccin\x20Latte\x2etheme\x1e\x7e/\x2econfig/fish/themes/Catppuccin\x20Macchiato\x2etheme\x1e\x7e/\x2econfig/fish/themes/Catppuccin\x20Mocha\x2etheme
 SETUVAR _fisher_jethrokuan_2F_z_files:\x7e/\x2econfig/fish/functions/__z\x2efish\x1e\x7e/\x2econfig/fish/functions/__z_add\x2efish\x1e\x7e/\x2econfig/fish/functions/__z_clean\x2efish\x1e\x7e/\x2econfig/fish/functions/__z_complete\x2efish\x1e\x7e/\x2econfig/fish/conf\x2ed/z\x2efish
 SETUVAR _fisher_jorgebucaran_2F_fisher_files:\x7e/\x2econfig/fish/functions/fisher\x2efish\x1e\x7e/\x2econfig/fish/completions/fisher\x2efish
 SETUVAR _fisher_patrickf1_2F_fzf_2E_fish_files:\x7e/\x2econfig/fish/functions/_fzf_configure_bindings_help\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_extract_var_info\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_preview_changed_file\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_preview_file\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_report_diff_type\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_report_file_type\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_directory\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_git_log\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_git_status\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_history\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_processes\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_search_variables\x2efish\x1e\x7e/\x2econfig/fish/functions/_fzf_wrapper\x2efish\x1e\x7e/\x2econfig/fish/functions/fzf_configure_bindings\x2efish\x1e\x7e/\x2econfig/fish/conf\x2ed/fzf\x2efish\x1e\x7e/\x2econfig/fish/completions/fzf_configure_bindings\x2efish
-SETUVAR _fisher_plugins:jorgebucaran/fisher\x1ejethrokuan/z\x1epatrickf1/fzf\x2efish\x1ecatppuccin/fish
+SETUVAR _fisher_plugins:jorgebucaran/fisher\x1ejethrokuan/z\x1epatrickf1/fzf\x2efish
 SETUVAR _fisher_upgraded_to_4_4:\x1d
-SETUVAR fish_color_autosuggestion:6c7086
+SETUVAR fish_color_autosuggestion:brblack
-SETUVAR fish_color_cancel:f38ba8
+SETUVAR fish_color_cancel:\x2d\x2dreverse
-SETUVAR fish_color_command:89b4fa
+SETUVAR fish_color_command:blue
-SETUVAR fish_color_comment:7f849c
+SETUVAR fish_color_comment:red
-SETUVAR fish_color_cwd:f9e2af
+SETUVAR fish_color_cwd:green
 SETUVAR fish_color_cwd_root:red
-SETUVAR fish_color_end:fab387
+SETUVAR fish_color_end:green
-SETUVAR fish_color_error:f38ba8
+SETUVAR fish_color_error:brred
-SETUVAR fish_color_escape:eba0ac
+SETUVAR fish_color_escape:brcyan
 SETUVAR fish_color_gray:6c7086
 SETUVAR fish_color_history_current:\x2d\x2dbold
-SETUVAR fish_color_host:89b4fa
+SETUVAR fish_color_host:normal
-SETUVAR fish_color_host_remote:a6e3a1
+SETUVAR fish_color_host_remote:\x1d
-SETUVAR fish_color_keyword:f38ba8
+SETUVAR fish_color_keyword:\x1d
-SETUVAR fish_color_normal:cdd6f4
+SETUVAR fish_color_match:\x2d\x2dbackground\x3dbrblue
-SETUVAR fish_color_operator:f5c2e7
+SETUVAR fish_color_normal:normal
-SETUVAR fish_color_option:a6e3a1
+SETUVAR fish_color_operator:brcyan
-SETUVAR fish_color_param:f2cdcd
+SETUVAR fish_color_option:\x1d
-SETUVAR fish_color_quote:a6e3a1
+SETUVAR fish_color_param:cyan
-SETUVAR fish_color_redirection:f5c2e7
+SETUVAR fish_color_quote:yellow
-SETUVAR fish_color_search_match:\x2d\x2dbackground\x3d313244
+SETUVAR fish_color_redirection:cyan\x1e\x2d\x2dbold
-SETUVAR fish_color_selection:\x2d\x2dbackground\x3d313244
+SETUVAR fish_color_search_match:bryellow\x1e\x2d\x2dbackground\x3dbrblack
+SETUVAR fish_color_selection:white\x1e\x2d\x2dbold\x1e\x2d\x2dbackground\x3dbrblack
 SETUVAR fish_color_status:f38ba8
-SETUVAR fish_color_user:94e2d5
+SETUVAR fish_color_user:brgreen
 SETUVAR fish_color_valid_path:\x2d\x2dunderline
 SETUVAR fish_key_bindings:fish_hybrid_key_bindings
 SETUVAR fish_pager_color_background:\x1d
-SETUVAR fish_pager_color_completion:cdd6f4
+SETUVAR fish_pager_color_completion:normal
-SETUVAR fish_pager_color_description:6c7086
+SETUVAR fish_pager_color_description:yellow\x1e\x2d\x2ditalics
-SETUVAR fish_pager_color_prefix:f5c2e7
+SETUVAR fish_pager_color_prefix:normal\x1e\x2d\x2dbold\x1e\x2d\x2dunderline
-SETUVAR fish_pager_color_progress:6c7086
+SETUVAR fish_pager_color_progress:brwhite\x1e\x2d\x2dbackground\x3dcyan
 SETUVAR fish_pager_color_secondary_background:\x1d
 SETUVAR fish_pager_color_secondary_completion:\x1d
 SETUVAR fish_pager_color_secondary_description:\x1d
 SETUVAR fish_pager_color_secondary_prefix:\x1d
-SETUVAR fish_pager_color_selected_background:\x1d
+SETUVAR fish_pager_color_selected_background:\x2d\x2dreverse
 SETUVAR fish_pager_color_selected_completion:\x1d
 SETUVAR fish_pager_color_selected_description:\x1d
 SETUVAR fish_pager_color_selected_prefix:\x1d

fish/.config/fish/functions/fisher.fish

@@ -1,6 +1,6 @@
 function fisher --argument-names cmd --description "A plugin manager for Fish"
     set --query fisher_path || set --local fisher_path $__fish_config_dir
-    set --local fisher_version 4.4.4
+    set --local fisher_version 4.4.5
     set --local fish_plugins $__fish_config_dir/fish_plugins
 
     switch "$cmd"
@@ -29,7 +29,7 @@ function fisher --argument-names cmd --description "A plugin manager for Fish"
             set --local old_plugins $_fisher_plugins
             set --local new_plugins
 
-            test -e $fish_plugins && set --local file_plugins (string match --regex -- '^[^\s]+$' <$fish_plugins)
+            test -e $fish_plugins && set --local file_plugins (string match --regex -- '^[^\s]+$' <$fish_plugins | string replace -- \~ ~)
 
             if ! set --query argv[2]
                 if test "$cmd" != update
@@ -206,7 +206,7 @@ function fisher --argument-names cmd --description "A plugin manager for Fish"
                     contains -- (string lower -- $plugin) (string lower -- $commit_plugins) || set --append commit_plugins $plugin
                 end
 
-                printf "%s\n" $commit_plugins >$fish_plugins
+                string replace --regex -- $HOME \~ $commit_plugins >$fish_plugins
             else
                 set --erase _fisher_plugins
                 command rm -f $fish_plugins

fish/.config/fish/themes/Catppuccin Frappe.theme

@@ -1,30 +0,0 @@
-# name: 'Catppuccin Frappé'
-# url: 'https://github.com/catppuccin/fish'
-# preferred_background: 303446
-
-fish_color_normal c6d0f5
-fish_color_command 8caaee
-fish_color_param eebebe
-fish_color_keyword e78284
-fish_color_quote a6d189
-fish_color_redirection f4b8e4
-fish_color_end ef9f76
-fish_color_comment 838ba7
-fish_color_error e78284
-fish_color_gray 737994
-fish_color_selection --background=414559
-fish_color_search_match --background=414559
-fish_color_option a6d189
-fish_color_operator f4b8e4
-fish_color_escape ea999c
-fish_color_autosuggestion 737994
-fish_color_cancel e78284
-fish_color_cwd e5c890
-fish_color_user 81c8be
-fish_color_host 8caaee
-fish_color_host_remote a6d189
-fish_color_status e78284
-fish_pager_color_progress 737994
-fish_pager_color_prefix f4b8e4
-fish_pager_color_completion c6d0f5
-fish_pager_color_description 737994

fish/.config/fish/themes/Catppuccin Latte.theme

@@ -1,30 +0,0 @@
-# name: 'Catppuccin Latte'
-# url: 'https://github.com/catppuccin/fish'
-# preferred_background: eff1f5
-
-fish_color_normal 4c4f69
-fish_color_command 1e66f5
-fish_color_param dd7878
-fish_color_keyword d20f39
-fish_color_quote 40a02b
-fish_color_redirection ea76cb
-fish_color_end fe640b
-fish_color_comment 8c8fa1
-fish_color_error d20f39
-fish_color_gray 9ca0b0
-fish_color_selection --background=ccd0da
-fish_color_search_match --background=ccd0da
-fish_color_option 40a02b
-fish_color_operator ea76cb
-fish_color_escape e64553
-fish_color_autosuggestion 9ca0b0
-fish_color_cancel d20f39
-fish_color_cwd df8e1d
-fish_color_user 179299
-fish_color_host 1e66f5
-fish_color_host_remote 40a02b
-fish_color_status d20f39
-fish_pager_color_progress 9ca0b0
-fish_pager_color_prefix ea76cb
-fish_pager_color_completion 4c4f69
-fish_pager_color_description 9ca0b0

fish/.config/fish/themes/Catppuccin Macchiato.theme

@@ -1,30 +0,0 @@
-# name: 'Catppuccin Macchiato'
-# url: 'https://github.com/catppuccin/fish'
-# preferred_background: 24273a
-
-fish_color_normal cad3f5
-fish_color_command 8aadf4
-fish_color_param f0c6c6
-fish_color_keyword ed8796
-fish_color_quote a6da95
-fish_color_redirection f5bde6
-fish_color_end f5a97f
-fish_color_comment 8087a2
-fish_color_error ed8796
-fish_color_gray 6e738d
-fish_color_selection --background=363a4f
-fish_color_search_match --background=363a4f
-fish_color_option a6da95
-fish_color_operator f5bde6
-fish_color_escape ee99a0
-fish_color_autosuggestion 6e738d
-fish_color_cancel ed8796
-fish_color_cwd eed49f
-fish_color_user 8bd5ca
-fish_color_host 8aadf4
-fish_color_host_remote a6da95
-fish_color_status ed8796
-fish_pager_color_progress 6e738d
-fish_pager_color_prefix f5bde6
-fish_pager_color_completion cad3f5
-fish_pager_color_description 6e738d

fish/.config/fish/themes/Catppuccin Mocha.theme

@@ -1,30 +0,0 @@
-# name: 'Catppuccin Mocha'
-# url: 'https://github.com/catppuccin/fish'
-# preferred_background: 1e1e2e
-
-fish_color_normal cdd6f4
-fish_color_command 89b4fa
-fish_color_param f2cdcd
-fish_color_keyword f38ba8
-fish_color_quote a6e3a1
-fish_color_redirection f5c2e7
-fish_color_end fab387
-fish_color_comment 7f849c
-fish_color_error f38ba8
-fish_color_gray 6c7086
-fish_color_selection --background=313244
-fish_color_search_match --background=313244
-fish_color_option a6e3a1
-fish_color_operator f5c2e7
-fish_color_escape eba0ac
-fish_color_autosuggestion 6c7086
-fish_color_cancel f38ba8
-fish_color_cwd f9e2af
-fish_color_user 94e2d5
-fish_color_host 89b4fa
-fish_color_host_remote a6e3a1
-fish_color_status f38ba8
-fish_pager_color_progress 6c7086
-fish_pager_color_prefix f5c2e7
-fish_pager_color_completion cdd6f4
-fish_pager_color_description 6c7086

nvim/.config/nvim/after/ftplugin/haskell.lua

@@ -0,0 +1 @@
+require('haskell-tools').lsp.start()

nvim/.config/nvim/ftdetect/metamath.vim

@@ -1,2 +0,0 @@
-au BufRead,BufNewFile *.mm set filetype=metamath
-au BufRead,BufNewFile *.mma set filetype=metamath

nvim/.config/nvim/init.lua

@@ -1,4 +1,4 @@
-require("wball.core.options")
+require('options')
-require("wball.core.keymaps")
+require('keymaps')
 
-require("wball.lazy")
+require('lazy_init')

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')

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 },
+})

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", {
+vim.api.nvim_create_autocmd('TermOpen', {
-    pattern = "*",
+    pattern = '*',
     callback = function()
         vim.opt.number = false
         vim.opt.relativenumber = false

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
+    }
+}

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({
+                    ['<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
+    }
+}

nvim/.config/nvim/lua/plugins/init.lua

@@ -0,0 +1,3 @@
+return {
+    'nvim-lua/plenary.nvim'
+}

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({
+                { '<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)",
+            },
+        },
+    }
+}

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' }
+    }
+}

nvim/.config/nvim/lua/plugins/languages/haskell.lua

@@ -0,0 +1,7 @@
+return {
+    {
+        'mrcjkb/haskell-tools.nvim',
+        version = '^4',
+        lazy = false,
+    }
+}

nvim/.config/nvim/lua/plugins/languages/init.lua

@@ -0,0 +1 @@
+return {}

nvim/.config/nvim/lua/plugins/languages/rust.lua

@@ -0,0 +1,7 @@
+return {
+    {
+        'mrcjkb/rustaceanvim',
+        version = '^5',
+        lazy = false
+    }
+}

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' },
+
+                        { '<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'
+    }
+}

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 = {
+            {
+                "<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'
+    }
+}

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'
+    }
+}

nvim/.config/nvim/lua/plugins/ui.lua

@@ -0,0 +1,6 @@
+return {
+    {
+        'stevearc/dressing.nvim',
+        opts = {},
+    }
+}

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({
+                { '<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
+    }
+}

nvim/.config/nvim/lua/wball/core/keymaps.lua

@@ -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" })

nvim/.config/nvim/lua/wball/lazy.lua

@@ -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,
-    },
-})

nvim/.config/nvim/lua/wball/plugins/autopairs.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/colorscheme.lua

@@ -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
-    }
-}

nvim/.config/nvim/lua/wball/plugins/comment.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/conform.lua

@@ -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",
-            },
-        }
-    }
-}

nvim/.config/nvim/lua/wball/plugins/dressing.lua

@@ -1,4 +0,0 @@
-return {
-    "stevearc/dressing.nvim",
-    event = "VeryLazy",
-}

nvim/.config/nvim/lua/wball/plugins/init.lua

@@ -1,3 +0,0 @@
-return {
-    "nvim-lua/plenary.nvim"
-}

nvim/.config/nvim/lua/wball/plugins/isabelle.lua

@@ -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
-    }
-}

nvim/.config/nvim/lua/wball/plugins/languages.lua

@@ -1,11 +0,0 @@
-return {
-    {
-        "whonore/Coqtail"
-    },
-    {
-        "https://git.sr.ht/~sircmpwn/hare.vim"
-    },
-    {
-        "https://git.sr.ht/~torresjrjr/vim-haredoc"
-    },
-}

nvim/.config/nvim/lua/wball/plugins/lsp/coq.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/lsp/haskell.lua

@@ -1,5 +0,0 @@
-return {
-    'mrcjkb/haskell-tools.nvim',
-    version = '^3',
-    ft = { 'haskell', 'lhaskell', 'cabal', 'cabalproject' },
-}

nvim/.config/nvim/lua/wball/plugins/lsp/lspconfig.lua

@@ -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,
-}

nvim/.config/nvim/lua/wball/plugins/lsp/miscutils.lua

@@ -1,6 +0,0 @@
-return {
-    {
-        "j-hui/fidget.nvim",
-        config = true,
-    },
-}

nvim/.config/nvim/lua/wball/plugins/lsp/rust.lua

@@ -1,4 +0,0 @@
-return {
-    'vxpm/ferris.nvim',
-    config = true,
-}

nvim/.config/nvim/lua/wball/plugins/neogit.lua

@@ -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
-    }
-}

nvim/.config/nvim/lua/wball/plugins/nvim-cmp.lua

@@ -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,
-}

nvim/.config/nvim/lua/wball/plugins/nvim-tree.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/sml.lua

@@ -1,5 +0,0 @@
-return {
-    {
-        'jez/vim-better-sml'
-    }
-}

nvim/.config/nvim/lua/wball/plugins/surround.lua

@@ -1,6 +0,0 @@
-return {
-    "kylechui/nvim-surround",
-    event = { "BufReadPre", "BufNewFile" },
-    version = "*",
-    config = true,
-}

nvim/.config/nvim/lua/wball/plugins/telescope.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/terminal.lua

@@ -1,12 +0,0 @@
-return {
-    {
-        "akinsho/toggleterm.nvim",
-        opts = {
-            open_mapping = [[<C-\>]],
-            direction = "horizontal",
-            insert_mappings = true,
-            start_in_insert = true,
-        },
-        keys = [[<C-\>]],
-    },
-}

nvim/.config/nvim/lua/wball/plugins/tmux.lua

@@ -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,
-}

nvim/.config/nvim/lua/wball/plugins/todo-comments.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/treesitter.lua

@@ -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
-}

nvim/.config/nvim/lua/wball/plugins/vifm.lua

@@ -1,3 +0,0 @@
-return {
-    "vifm/vifm.vim",
-}

nvim/.config/nvim/lua/wball/plugins/which-key.lua

@@ -1,9 +0,0 @@
-return {
-    "folke/which-key.nvim",
-    event = "VeryLazy",
-    init = function()
-        vim.o.timeout = true
-        vim.o.timeoutlen = 500
-    end,
-    opts = {}
-}

nvim/.config/nvim/syntax/metamath.vim

@@ -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
-