From f00471832590fde38c6dc1848fd5fade29b80f6f Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 28 May 2021 14:17:40 +0200
Subject: [PATCH] vimrc: update diags in insert mode

---
 vimrc | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

diff --git a/vimrc b/vimrc
index 72e5c30..0b54fac 100644
--- a/vimrc
+++ b/vimrc
@@ -181,6 +181,7 @@ call tcomment#type#Define('nix', '# %s')
 call tcomment#type#Define('chaskell', '-- %s')
 call tcomment#type#Define('vala', '// %s')
 call tcomment#type#Define('tptp', '%% %s')
+call tcomment#type#Define('lean', '-- %s')
 
 au syntax tex setl iskeyword+=:
 au syntax tex syn region texZone start="\\begin{clilisting}" end="\\end{clilisting}\|%stopzone\>"
@@ -264,6 +265,22 @@ require'compe'.setup {
   };
 }
 
+vim.lsp.handlers["textDocument/publishDiagnostics"] = vim.lsp.with(
+  vim.lsp.diagnostic.on_publish_diagnostics, {
+    -- Enable underline, use default values
+    underline = true,
+    -- Enable virtual text, override spacing to 4
+    virtual_text = {
+      spacing = 4,
+    },
+    -- Use a function to dynamically turn signs off
+    -- and on, using buffer local variables
+    -- signs = function(bufnr, client_id)
+    --   return vim.bo[bufnr].show_signs == false
+    -- end,
+    update_in_insert = true,
+  })
+
 local luadev = require("lua-dev").setup({
   lspconfig = {
     cmd = {"lua-language-server"}