From 2af32e0a2368d47d898abd70b043280c3871ece6 Mon Sep 17 00:00:00 2001 From: utensil Date: Tue, 22 Oct 2024 22:54:34 +0800 Subject: [PATCH] Add a default mapping for `:LeanRestartFile` and related tips --- README.md | 4 ++++ lua/lean/init.lua | 5 +++++ 2 files changed, 9 insertions(+) diff --git a/README.md b/README.md index 2bd979f3..3067ce6c 100644 --- a/README.md +++ b/README.md @@ -139,12 +139,16 @@ This can be configured by putting a line at the top of your `~/.config/nvim/init | `v` | interactively configure infoview view options | | `` | jump into the infoview window associated with the current lean file | | `\\` | show what abbreviation produces the symbol under the cursor | +| `r` | Restart the Lean server for the current file. | > [!TIP] > See `:help ` if you haven't previously interacted with the local leader key. > Some nvim users remap this key to make it easier to reach, so you may want to consider what key that means for your own keyboard layout. > My (Julian's) `` is set to ``, and my `` to ``, which may be a good choice for you if you have no other preference. +> [!TIP] +> If you are also looking for a way to restart the Lean server, you can use the `:LspRestart` command, or map it to a key of your choice. It will restart the language servers for the current buffer/file, so this also applies to other language servers you may be using. + ### In Infoview Windows | Key | Function | diff --git a/lua/lean/init.lua b/lua/lean/init.lua index 27712b12..4958c6eb 100644 --- a/lua/lean/init.lua +++ b/lua/lean/init.lua @@ -81,6 +81,11 @@ local lean = { 'LeanAbbreviationsReverseLookup', { desc = 'Show how to type the unicode character under the cursor.' }, }, + { + 'r', + 'LeanRestartFile', + { desc = 'Restart the Lean server for the current file.' }, + }, }, }