support post-code-action hooks.

[mattpolzin]

I will be far from offended if this isn't the direction you want to go with this, but if you do I am also happy to add some documentation for it.

In playing around locally, this works rather well for me and it's extensible, although it doesn't work with "multiple result" actions as-is.

local filters = require('idris2.code_action').filters

local save_hook = function(err, result, ctx, config)
  vim.cmd('write')
end

local post_hooks = {
  [filters.CASE_SPLIT] = save_hook,
  [filters.MAKE_LEMMA] = save_hook,
  [filters.ADD_CLAUSE] = save_hook
}

require('idris2').setup({
  server = {on_attach = custom_lsp_attach},
  post_hooks = post_hooks
})

[mattpolzin]

Darn, I am mostly done with the code changes, but hit this rather substantial consideration that means I cannot simply override the default codeAction handler as simply as can be done for hover: https://github.com/neovim/neovim/issues/15848

Will look into it more a bit later.

[mattpolzin]

I'm not sure we want to rewrite the whole neovim handling of code actions just to get this to work... I tried hooking into just vim.ui.select and that works (we can even make sure the select was triggered as part of code actions) but I don't think there's a way to know which code action in this case. We could backtrack a tad and decide there's just a single post_code_action_handler that runs after all code actions rather than knowing which one; in that case it would be easy enough to do by overriding vim.ui.select.

[mattpolzin]

Ok, my vote is currently to implement this as a one-size-fits all post hook. It's not the best, but because I don't want to call "write" after a make case or make with (because they inevitably result in programs that won't compile until blanks are filled in), I can do a string match on the selected tuple title. Janky, but functional.

[mattpolzin]

Well, that latest commit would be the other option (single hook) that seems to be working pretty well for me with the following post hook (that could be simplified to just always save, but I definitely prefer not saving on make case and make with commands).

local save_hook = function(action)
  if string.match(action.title, "Make case")
     or string.match(action.title, "Make with") then
       return
  end
  vim.cmd('sleep 10m')
  vim.cmd('silent write')
end

require('idris2').setup({
  code_action_post_hook = save_hook
})

[ShinKage]

Since I don't like the idea of copying the default handler, and we may still have a different or customizable UI for code actions, the single global hook is the best idea currently. However it may be a good idea to provide a set of predicates so that we don't directly expose to the user the janky way of checking the executed code action.

[mattpolzin]

I wonder if the edit kind (e.g. refactor.extract) will be a good start to surface predicates on. Haven't looked to see if these differentiate the actions enough for what I am trying to do myself but they might.

[ShinKage]

I don't think kind are sufficient. For compatibility reason with some editors we only send the default ones even if we can filter with more specific kinds.

[mattpolzin]

Here's where I landed then. I will document this if you think it looks ready otherwise.

Example usage:

local introspect = require('idris2.code_action').introspect_filter
local filters = require('idris2.code_action').filters

local save_hook = function(action)
  if introspect(action) == filters.MAKE_CASE
    or introspect(action) == filters.MAKE_WITH then
      return
  end
  vim.cmd('sleep 10m')
  vim.cmd('silent write')
end

require('idris2').setup({
  code_action_post_hook = save_hook
})

[ShinKage]

Looks good to me. 👍