vimrc: use lsp

vimrc

@@ -9,8 +9,6 @@ Plug 'nathanaelkane/vim-indent-guides'
 
 Plug 'chrisbra/Recover.vim'
 
-" Plug 'Valloric/YouCompleteMe', { 'do': './install.sh --clang-completer --system-libclang' }
-
 Plug 'Shougo/vimproc.vim' , { 'do': 'make -f make_unix.mak' }
 
 Plug 'junegunn/fzf', { 'dir': '~/.fzf' }
@@ -25,8 +23,6 @@ Plug 'bling/vim-airline'
 Plug 'tomtom/tcomment_vim'
 " Plug 'jalcine/cmake.vim' --slow
 
-" Plug 'roxma/nvim-completion-manager'
-
 Plug 'editorconfig/editorconfig-vim'
 " vim-sleuth?
 
@@ -36,7 +32,6 @@ Plug 'mtscout6/vim-cjsx'
 Plug 'mxw/vim-jsx'
 Plug 'othree/html5.vim'
 Plug 'digitaltoad/vim-jade'
-" Plug 'marijnh/tern_for_vim'
 
 Plug 'ledger/vim-ledger'
 
@@ -98,19 +93,10 @@ Plug 'c-cube/vim-tptp'
 
 Plug 'sirtaj/vim-openscad'
 
-Plug 'SirVer/ultisnips'
-Plug 'honza/vim-snippets'
-
 Plug 'nanotech/jellybeans.vim'
 Plug 'sonph/onehalf', { 'rtp': 'vim' }
 
-Plug '~/dgapt', { 'rtp': 'vim' }
+" Plug '~/dgapt', { 'rtp': 'vim' }
-" Plug '~/lean.vim'
-Plug 'leanprover/lean.vim'
-
-" Plug 'neoclide/coc.nvim', {'do': { -> coc#util#install()}}
-" Plug 'autozimu/LanguageClient-neovim', { 'do': ':UpdateRemotePlugins' }
-Plug 'Shougo/echodoc.vim'
 
 Plug 'rickhowe/diffchar.vim'
 
@@ -126,6 +112,23 @@ Plug 'elixir-editors/vim-elixir'
 
 " Plug 'glacambre/firenvim', { 'do': { _ -> firenvim#install(0) } }
 
+if has('nvim-0.5')
+
+Plug 'nvim-treesitter/nvim-treesitter', {'do': ':TSUpdate'}
+Plug 'nvim-treesitter/nvim-treesitter-textobjects'
+Plug 'nvim-treesitter/playground'
+
+Plug 'hrsh7th/nvim-compe'
+if isdirectory(expand('~/lean.nvim'))
+  Plug '~/lean.nvim'
+else
+  " Plug 'Julian/lean.nvim'
+  Plug 'gebner/lean.nvim'
+endif
+Plug 'neovim/nvim-lspconfig'
+
+endif
+
 call plug#end()
 
 filetype plugin indent on
@@ -190,17 +193,83 @@ au FileChangedRO * set noreadonly
 
 nnoremap <c-p> :FZF<cr>
 
-" nnoremap <silent> K :call LanguageClient_textDocument_hover()<CR>
+if has('nvim-0.5')
-" nnoremap <silent> gd :call LanguageClient_textDocument_definition()<CR>
+lua <<EOF
+  require('lean').setup{
+    treesitter = {},
+    lsp = {
+      on_attach = function(client, bufnr)
+        -- See https://github.com/neovim/nvim-lspconfig#keybindings-and-completion
+        -- for detailed examples of what you may want to do here.
+        --
+        -- Mapping a key (typically K) to `vim.lsp.buf.hover()`
+        -- is highly recommended for Lean, since the hover LSP command
+        -- is where you'll see the current goal state.
+        --
+        -- You may furthermore want to add an `autocmd` to run it on
+        -- `CursorHoldI`, which will show the goal state any time the
+        -- cursor is unmoved in insert mode.
+        --
+        -- In the future, this plugin may offer a recommended "complete
+        -- setup" for easy enabling of the above.
+        local function buf_set_keymap(...) vim.api.nvim_buf_set_keymap(bufnr, ...) end
+        local function buf_set_option(...) vim.api.nvim_buf_set_option(bufnr, ...) end
+        buf_set_keymap('n', 'gd', '<Cmd>lua vim.lsp.buf.definition()<CR>', {noremap = true})
+        buf_set_keymap('n', 'K', '<Cmd>lua vim.lsp.buf.hover()<CR>', {noremap = true})
+        buf_set_option('omnifunc', 'v:lua.vim.lsp.omnifunc')
+	vim.api.nvim_exec([[
+	  augroup lsp_document_highlight
+	    autocmd!
+	    autocmd CursorHold <buffer> lua vim.lsp.buf.document_highlight()
+	    autocmd CursorMoved <buffer> lua vim.lsp.buf.clear_references()
+	  augroup END
+	]], false)
+      end,
+      init_options = {
+        semanticHighlighting = true,
+      },
+      cmd = {"lean", "--server"},
+    },
+  }
 
-" let g:cm_completekeys = "\<Plug>(cm_completefunc)"
+  require('nvim-treesitter.configs').setup{
+    -- playground = {
+    --   enable = true,
+    --   disable = {},
+    --   updatetime = 25,
+    -- },
+    -- query_linter = {
+    --   enable = true,
+    --   use_virtual_text = true,
+    --   lint_events = {"BufWrite", "CursorHold"},
+    -- },
+    highlight = { enable = true },
+    indent = { enable = true },
+    textobjects = {
+      select = {
+	enable = true,
+	keymaps = {
+	  ["af"] = "@function.outer",
+	  ["if"] = "@function.inner",
+	  ["ac"] = "@class.outer",
+	  ["ic"] = "@class.inner",
+	  ["aa"] = "@parameter.outer",
+	  ["ia"] = "@parameter.inner",
+	},
+      },
+    },
+  }
 
-" " call LanguageClient_setLoggingLevel('DEBUG')
+EOF
-" let g:LanguageClient_trace = 'verbose'
+
-" let g:LanguageClient_autoStart = 1
+hi LspReferenceRead cterm=bold ctermbg=red guibg=LightYellow
-" let g:LanguageClient_serverCommands = {
+hi LspReferenceText cterm=bold ctermbg=red guibg=LightYellow
-"     \ 'lean': ['node', '/home/gebner/lean-client-js/lean-language-server/lib/index.js', '--stdio'],
+hi LspReferenceWrite cterm=bold ctermbg=red guibg=LightYellow
-"     \ }
+hi LspDiagnosticsDefaultError cterm=bold ctermfg=Red
+hi LspDiagnosticsDefaultWarning cterm=bold ctermfg=Yellow
+hi LspDiagnosticsDefaultInformation ctermfg=Blue
+
+endif
 
 let g:gutentags_cache_dir="~/.config/nvim/gutentags"
 
@@ -220,66 +289,3 @@ augroup my_cm_setup
 	\ 'cm_refresh': {'omnifunc': 'vimtex#complete#omnifunc'},
 	\ })
 augroup END
-
-" " coc.nvim
-"
-"
-" inoremap <silent><expr> <c-space> coc#refresh()
-"
-" " Use <cr> for confirm completion, `<C-g>u` means break undo chain at current position.
-" " Coc only does snippet and additional edit on confirm.
-" inoremap <expr> <cr> pumvisible() ? "\<C-y>" : "\<C-g>u\<CR>"
-"
-" " Use `[c` and `]c` for navigate diagnostics
-" nmap <silent> [c <Plug>(coc-diagnostic-prev)
-" nmap <silent> ]c <Plug>(coc-diagnostic-next)
-"
-" " Remap keys for gotos
-" nmap <silent> gd <Plug>(coc-definition)
-" nmap <silent> gy <Plug>(coc-type-definition)
-" nmap <silent> gi <Plug>(coc-implementation)
-" nmap <silent> gr <Plug>(coc-references)
-"
-" " Use K for show documentation in preview window
-" nnoremap <silent> K :call <SID>show_documentation()<CR>
-"
-" function! s:show_documentation()
-"   if &filetype == 'vim'
-"     execute 'h '.expand('<cword>')
-"   else
-"     call CocAction('doHover')
-"   endif
-" endfunction
-"
-" " Highlight symbol under cursor on CursorHold
-" autocmd CursorHold * silent call CocActionAsync('highlight')
-"
-" " Remap for rename current word
-" nmap <leader>rn <Plug>(coc-rename)
-"
-" " Remap for format selected region
-" vmap <leader>f  <Plug>(coc-format-selected)
-" nmap <leader>f  <Plug>(coc-format-selected)
-"
-" augroup mygroup
-"   autocmd!
-"   " Setup formatexpr specified filetype(s).
-"   autocmd FileType typescript,json setl formatexpr=CocAction('formatSelected')
-"   " Update signature help on jump placeholder
-"   autocmd User CocJumpPlaceholder call CocActionAsync('showSignatureHelp')
-" augroup end
-"
-" " Remap for do codeAction of selected region, ex: `<leader>aap` for current paragraph
-" vmap <leader>a  <Plug>(coc-codeaction-selected)
-" nmap <leader>a  <Plug>(coc-codeaction-selected)
-"
-" " Remap for do codeAction of current line
-" nmap <leader>ac  <Plug>(coc-codeaction)
-" " Fix autofix problem of current line
-" nmap <leader>qf  <Plug>(coc-fix-current)
-"
-" " Use `:Format` for format current buffer
-" command! -nargs=0 Format :call CocAction('format')
-"
-" " Use `:Fold` for fold current buffer
-" command! -nargs=? Fold :call     CocAction('fold', <f-args>)