Remove the mapping for sorry filling.

We have code actions now for doing this. We'll leave the functionality present for a bit longer to see if it's useful for anything. If you want a mapping you can map LeanSorryFill.
Julian · Jun 3, 2024 · dab10cc · dab10cc · MithicSpirit · Jun 5, 2024
1 parent 6781f42
commit dab10cc
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 3 deletions.
diff --git a/README.rst b/README.rst
@@ -146,8 +146,6 @@ This can be configured by putting a line at the top of your ``~/.config/nvim/ini
 +------------------------+----------------------------------------------------+
 | ``<LocalLeader>dt``    | toggle auto diff pin mode without clearing diff pin|
 +------------------------+----------------------------------------------------+
-| ``<LocalLeader>s``     | insert a ``sorry`` for each open goal              |
-+------------------------+----------------------------------------------------+
 | ``<LocalLeader><Tab>`` | jump into the infoview window associated with the  |
 |                        | current lean file                                  |
 +------------------------+----------------------------------------------------+

diff --git a/lua/lean/init.lua b/lua/lean/init.lua
@@ -26,7 +26,6 @@ local lean = {
       ['<LocalLeader>w'] = '<Cmd>LeanInfoviewEnableWidgets<CR>',
       ['<LocalLeader>W'] = '<Cmd>LeanInfoviewDisableWidgets<CR>',
       ['<LocalLeader><Tab>'] = '<Cmd>LeanGotoInfoview<CR>',
-      ['<LocalLeader>s'] = '<Cmd>LeanSorryFill<CR>',
       ['<LocalLeader>\\'] = '<Cmd>LeanAbbreviationsReverseLookup<CR>',
     },
     i = {},