diff --git a/README.md b/README.md
index 5fae2aa..4126359 100644
--- a/README.md
+++ b/README.md
@@ -33,17 +33,18 @@ exposed via vim commands. Most commands have an equivalent in [agda-mode].
| Vim command | Description | Equivalent agda-mode keybinding |
| :--- | :--- | :--- |
-| `:CornelisLoad` | Load and type-check buffer | C-cC-l |
-| `:CornelisGoals` | Show all goals | C-cC-? |
-| `:CornelisRestart` | Kill and restart the `agda` process | C-cC-xC-r |
-| `:CornelisAbort` | Abort running command | C-cC-xC-a |
-| `:CornelisSolve ` | Solve constraints | C-cC-s |
-| `:CornelisGoToDefinition` | Jump to definition of name at cursor | M-. or middle mouse button |
-| `:CornelisPrevGoal` | Jump to previous goal | C-cC-b |
-| `:CornelisNextGoal` | Jump to next goal | C-cC-f |
-| `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ |
-| `:CornelisInc` | Like `` but also targets sub- and superscripts | _(none)_ |
-| `:CornelisDec` | Like `` but also targets sub- and superscripts | _(none)_ |
+| `:CornelisLoad` | Load and type-check buffer | C-cC-l |
+| `:CornelisGoals` | Show all goals | C-cC-? |
+| `:CornelisRestart` | Kill and restart the `agda` process | C-cC-xC-r |
+| `:CornelisAbort` | Abort running command | C-cC-xC-a |
+| `:CornelisSolve ` | Solve constraints | C-cC-s |
+| `:CornelisGoToDefinition` | Jump to definition of name at cursor | M-. or middle mouse button |
+| `:CornelisPrevGoal` | Jump to previous goal | C-cC-b |
+| `:CornelisNextGoal` | Jump to next goal | C-cC-f |
+| `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ |
+| `:CornelisInc` | Like `` but also targets sub- and superscripts | _(none)_ |
+| `:CornelisDec` | Like `` but also targets sub- and superscripts | _(none)_ |
+| `:CornelisCloseInfoWindows` | Close (all) info windows cornelis has opened | _(none)_ |
### Commands in context of a goal
@@ -287,6 +288,7 @@ for it! This is enough to get you started:
```viml
au BufRead,BufNewFile *.agda call AgdaFiletype()
+au QuitPre *.agda :CornelisCloseInfoWindows
function! AgdaFiletype()
nnoremap l :CornelisLoad
nnoremap r :CornelisRefine
diff --git a/src/Lib.hs b/src/Lib.hs
index 7b3b07a..13f7513 100644
--- a/src/Lib.hs
+++ b/src/Lib.hs
@@ -200,29 +200,30 @@ cornelis = do
wrapPlugin $ Plugin
{ environment = env
, exports =
- [ $(command "CornelisRestart" 'doRestart) [CmdSync Async]
- , $(command "CornelisAbort" 'doAbort) [CmdSync Async]
- , $(command "CornelisLoad" 'doLoad) [CmdSync Async]
- , $(command "CornelisGoals" 'doAllGoals) [CmdSync Async]
- , $(command "CornelisSolve" 'solveOne) [CmdSync Async, rw_complete]
- , $(command "CornelisAuto" 'autoOne) [CmdSync Async]
- , $(command "CornelisTypeInfer" 'doTypeInfer) [CmdSync Async]
- , $(command "CornelisTypeContext" 'typeContext) [CmdSync Async, rw_complete]
- , $(command "CornelisTypeContextInfer" 'typeContextInfer) [CmdSync Async, rw_complete]
- , $(command "CornelisMakeCase" 'doCaseSplit) [CmdSync Async]
- , $(command "CornelisRefine" 'doRefine) [CmdSync Async]
- , $(command "CornelisGive" 'doGive) [CmdSync Async]
- , $(command "CornelisElaborate" 'doElaborate) [CmdSync Async, rw_complete]
- , $(command "CornelisPrevGoal" 'doPrevGoal) [CmdSync Async]
- , $(command "CornelisNextGoal" 'doNextGoal) [CmdSync Async]
- , $(command "CornelisGoToDefinition" 'doGotoDefinition) [CmdSync Async]
- , $(command "CornelisWhyInScope" 'doWhyInScope) [CmdSync Async]
- , $(command "CornelisNormalize" 'doNormalize) [CmdSync Async, cm_complete]
- , $(command "CornelisHelperFunc" 'doHelperFunc) [CmdSync Async, rw_complete]
- , $(command "CornelisQuestionToMeta" 'doQuestionToMeta) [CmdSync Async]
- , $(command "CornelisInc" 'doIncNextDigitSeq) [CmdSync Async]
- , $(command "CornelisDec" 'doDecNextDigitSeq) [CmdSync Async]
- , $(command "CornelisDebug" 'doDebug) [CmdSync Async, debug_complete]
+ [ $(command "CornelisRestart" 'doRestart) [CmdSync Async]
+ , $(command "CornelisAbort" 'doAbort) [CmdSync Async]
+ , $(command "CornelisLoad" 'doLoad) [CmdSync Async]
+ , $(command "CornelisGoals" 'doAllGoals) [CmdSync Async]
+ , $(command "CornelisSolve" 'solveOne) [CmdSync Async, rw_complete]
+ , $(command "CornelisAuto" 'autoOne) [CmdSync Async]
+ , $(command "CornelisTypeInfer" 'doTypeInfer) [CmdSync Async]
+ , $(command "CornelisTypeContext" 'typeContext) [CmdSync Async, rw_complete]
+ , $(command "CornelisTypeContextInfer" 'typeContextInfer) [CmdSync Async, rw_complete]
+ , $(command "CornelisMakeCase" 'doCaseSplit) [CmdSync Async]
+ , $(command "CornelisRefine" 'doRefine) [CmdSync Async]
+ , $(command "CornelisGive" 'doGive) [CmdSync Async]
+ , $(command "CornelisElaborate" 'doElaborate) [CmdSync Async, rw_complete]
+ , $(command "CornelisPrevGoal" 'doPrevGoal) [CmdSync Async]
+ , $(command "CornelisNextGoal" 'doNextGoal) [CmdSync Async]
+ , $(command "CornelisGoToDefinition" 'doGotoDefinition) [CmdSync Async]
+ , $(command "CornelisWhyInScope" 'doWhyInScope) [CmdSync Async]
+ , $(command "CornelisNormalize" 'doNormalize) [CmdSync Async, cm_complete]
+ , $(command "CornelisHelperFunc" 'doHelperFunc) [CmdSync Async, rw_complete]
+ , $(command "CornelisQuestionToMeta" 'doQuestionToMeta) [CmdSync Async]
+ , $(command "CornelisInc" 'doIncNextDigitSeq) [CmdSync Async]
+ , $(command "CornelisDec" 'doDecNextDigitSeq) [CmdSync Async]
+ , $(command "CornelisDebug" 'doDebug) [CmdSync Async, debug_complete]
+ , $(command "CornelisCloseInfoWindows" 'doCloseInfoWindows) [CmdSync Sync]
, $(function "InternalCornelisRewriteModeCompletion" 'rewriteModeCompletion) Sync
, $(function "InternalCornelisComputeModeCompletion" 'computeModeCompletion) Sync
, $(function "InternalCornelisDebugCommandCompletion" 'debugCommandCompletion) Sync
diff --git a/src/Plugin.hs b/src/Plugin.hs
index c3354dc..6c2b907 100644
--- a/src/Plugin.hs
+++ b/src/Plugin.hs
@@ -13,7 +13,7 @@ import Cornelis.Agda (withCurrentBuffer, runIOTCM, withAgda, getAgda)
import Cornelis.Diff (resetDiff, recordUpdate, Replace(..), Colline(..), Vallee(..))
import Cornelis.Goals
import Cornelis.Highlighting (getExtmarks, highlightInterval, updateLineIntervals)
-import Cornelis.InfoWin (showInfoWindow)
+import Cornelis.InfoWin (showInfoWindow, closeInfoWindows)
import Cornelis.Offsets
import Cornelis.Pretty (prettyGoals, HighlightGroup (CornelisHole))
import Cornelis.Types
@@ -378,3 +378,6 @@ notifyEdit _ buf _ sr sc _ er ec _ fr fc _ = do
where
pos l c = Colline (toZeroIndexed l) (toZeroIndexed c)
range l c = Vallee (Offset l) (Offset c)
+
+doCloseInfoWindows :: CommandArguments -> Neovim CornelisEnv ()
+doCloseInfoWindows = const closeInfoWindows