Fix idempotency issue

It turns out that most of these come from the `_DEFAULTS` pattern. This
is because of the following:
original state:
```lua
tbl = { _DEFAULTS = ... }
```
after configuration with empty table, `tbl = vim.tbl_extend(tbl._DEFAULTS, {})`
which practically replaces `tbl` by `tbl._DEFAULTS`:
```lua
tbl = { ... }
```
after this, the next call to `vim.tbl_extend(tbl._DEFAULTS, {})` fails, as
`tbl._DEFAULTS` is nil.

The solution to this is to just call `vim.tbl_extend(tbl, ...)` and store the
defaults in `tbl` itself. The `._DEFAULTS` field can be preserved by copying to
it after initialization.

Also `command` has been replaced with `command!` in vimscript and
`autocmd`s have been wrapped in an `augroup` which resets its state each
call. This is also common practice that avoids duplicate autocommands.

Fixes Julian#145

lua/lean/commands.lua

@@ -116,11 +116,11 @@ end
 
 function commands.enable()
   vim.cmd[[
-    command LeanPlainGoal :lua require'lean.commands'.show_goal(false)
-    command LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
-    command LeanGoal :lua require'lean.commands'.show_goal()
-    command LeanTermGoal :lua require'lean.commands'.show_term_goal()
-    command LeanLineDiagnostics :lua require'lean.commands'.show_line_diagnostics()
+    command! LeanPlainGoal :lua require'lean.commands'.show_goal(false)
+    command! LeanPlainTermGoal :lua require'lean.commands'.show_term_goal(false)
+    command! LeanGoal :lua require'lean.commands'.show_goal()
+    command! LeanTermGoal :lua require'lean.commands'.show_term_goal()
+    command! LeanLineDiagnostics :lua require'lean.commands'.show_line_diagnostics()
   ]]
 end
 

lua/lean/ft.lua

@@ -21,7 +21,7 @@ function ft.enable(opts)
     -- this means we have to manage it
     global_default_managed = true
   end
-  options= vim.tbl_extend("force", options._DEFAULTS, opts)
+  options= vim.tbl_extend("force", options, opts)
   if global_default_managed then
     lean_nvim_default_filetype = options.default
   end

lua/lean/infoview.lua

@@ -20,7 +20,6 @@ local infoview = {
   debug = false,
 }
 local options = {
-  _DEFAULTS = {
     width = 50,
     height = 20,
     horizontal_position = 'bottom',
@@ -46,7 +45,6 @@ local options = {
       ['C'] = 'clear_all',
       ['<LocalLeader><Tab>'] = 'goto_last_window',
     }
-  }
 }
 
 --- An individual pin.
@@ -1039,13 +1037,13 @@ end
 
 --- Enable and open the infoview across all Lean buffers.
 function infoview.enable(opts)
-  options = vim.tbl_extend("force", options._DEFAULTS, opts)
+  options = vim.tbl_extend("force", options, opts)
   infoview.mappings = options.mappings
   infoview.enabled = true
   infoview.set_autoopen(options.autoopen)
   set_augroup("LeanInfoviewInit", [[
-    autocmd FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
-    autocmd FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean3 lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
+    autocmd! FileType lean lua require'lean.infoview'.make_buffer_focusable(vim.fn.expand('<afile>'))
   ]])
 end
 

lua/lean/init.lua

@@ -43,7 +43,6 @@ function lean.setup(opts)
 
   opts.infoview = opts.infoview or {}
   require'lean.infoview'.enable(opts.infoview)
-
   require'lean.commands'.enable()
 
   opts.lsp3 = opts.lsp3 or {}
@@ -64,31 +63,34 @@ function lean.setup(opts)
   if opts.stderr.enable ~= false then require'lean.stderr'.enable(opts.stderr or {}) end
 
   vim.cmd[[
-    command LeanRestartFile :lua require'lean.lsp'.restart_file()
-    command LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file()
-
-    command LeanInfoviewToggle :lua require'lean.infoview'.toggle()
-    command LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause()
-    command LeanInfoviewAddPin :lua require'lean.infoview'.add_pin()
-    command LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins()
-    command LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin()
-    command LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin()
-    command LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true)
-    command LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false)
-    command LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets()
-    command LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets()
-    command LeanGotoInfoview :lua require'lean.infoview'.go_to()
-
-    command LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup()
-
-    command LeanSorryFill :lua require'lean.sorry'.fill()
-    command LeanTryThis :lua require'lean.trythis'.swap()
+    command! LeanRestartFile :lua require'lean.lsp'.restart_file()
+    command! LeanRefreshFileDependencies :lua require'lean.lsp'.restart_file()
+
+    command! LeanInfoviewToggle :lua require'lean.infoview'.toggle()
+    command! LeanInfoviewPinTogglePause :lua require'lean.infoview'.pin_toggle_pause()
+    command! LeanInfoviewAddPin :lua require'lean.infoview'.add_pin()
+    command! LeanInfoviewClearPins :lua require'lean.infoview'.clear_pins()
+    command! LeanInfoviewSetDiffPin :lua require'lean.infoview'.set_diff_pin()
+    command! LeanInfoviewClearDiffPin :lua require'lean.infoview'.clear_diff_pin()
+    command! LeanInfoviewToggleAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(true)
+    command! LeanInfoviewToggleNoClearAutoDiffPin :lua require'lean.infoview'.toggle_auto_diff_pin(false)
+    command! LeanInfoviewEnableWidgets :lua require'lean.infoview'.enable_widgets()
+    command! LeanInfoviewDisableWidgets :lua require'lean.infoview'.disable_widgets()
+    command! LeanGotoInfoview :lua require'lean.infoview'.go_to()
+
+    command! LeanAbbreviationsReverseLookup :lua require'lean.abbreviations'.show_reverse_lookup()
+
+    command! LeanSorryFill :lua require'lean.sorry'.fill()
+    command! LeanTryThis :lua require'lean.trythis'.swap()
   ]]
 
   if opts.mappings == true then
     vim.cmd[[
-      autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true)
-      autocmd FileType lean lua require'lean'.use_suggested_mappings(true)
+      augroup lean_nvim_mappings
+        autocmd!
+        autocmd FileType lean3 lua require'lean'.use_suggested_mappings(true)
+        autocmd FileType lean lua require'lean'.use_suggested_mappings(true)
+      augroup END
     ]]
   end
 

lua/lean/progress_bars.lua

@@ -1,7 +1,8 @@
 local progress = require('lean.progress')
 
-local M = {}
-local options = { _DEFAULTS = { priority = 10, character = '⋯' } }
+local progress_bars = {}
+local options = {  priority = 10, character = '⋯' }
+options._DEFAULTS = vim.deepcopy(options)
 
 local sign_group_name = 'leanSignProgress'
 local sign_name = 'leanSignProgress'
@@ -41,8 +42,8 @@ end
 -- Table from bufnr to timer object.
 local timers = {}
 
-function M.update(params)
-  if not M.enabled then return end
+function progress_bars.update(params)
+  if not progress_bars.enabled then return end
   -- TODO FIXME can potentially create new buffer
   local bufnr = vim.uri_to_bufnr(params.textDocument.uri)
 
@@ -54,15 +55,15 @@ function M.update(params)
   end
 end
 
-function M.enable(opts)
-  options = vim.tbl_extend("force", options._DEFAULTS, opts)
+function progress_bars.enable(opts)
+  options = vim.tbl_extend("force", options, opts)
 
   vim.fn.sign_define(sign_name, {
     text = options.character,
     texthl = 'leanSignProgress',
   })
   vim.cmd[[hi def leanSignProgress guifg=orange ctermfg=215]]
-  M.enabled = true
+  progress_bars.enabled = true
 end
 
-return M
+return progress_bars