Skip to content

Commit

Permalink
Merge pull request #143 from silky/auto-close-info-window
Browse files Browse the repository at this point in the history 
Auto-close the info window, when closing the current buffer.
  • Loading branch information
@isovector
isovector authored Mar 2, 2024
2 parents ed9d12f + 320bde7 commit 9d83faa
Show file tree
Hide file tree
Showing 3 changed files with 41 additions and 35 deletions.
24 changes: 13 additions & 11 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 | <kbd>C-c</kbd><kbd>C-l</kbd> |
| `:CornelisGoals` | Show all goals | <kbd>C-c</kbd><kbd>C-?</kbd> |
| `:CornelisRestart` | Kill and restart the `agda` process | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-r</kbd> |
| `:CornelisAbort` | Abort running command | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-a</kbd> |
| `:CornelisSolve <RW>` | Solve constraints | <kbd>C-c</kbd><kbd>C-s</kbd> |
| `:CornelisGoToDefinition` | Jump to definition of name at cursor | <kbd>M-.</kbd> or middle mouse button |
| `:CornelisPrevGoal` | Jump to previous goal | <kbd>C-c</kbd><kbd>C-b</kbd> |
| `:CornelisNextGoal` | Jump to next goal | <kbd>C-c</kbd><kbd>C-f</kbd> |
| `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ |
| `:CornelisInc` | Like `<C-A>` but also targets sub- and superscripts | _(none)_ |
| `:CornelisDec` | Like `<C-X>` but also targets sub- and superscripts | _(none)_ |
| `:CornelisLoad` | Load and type-check buffer | <kbd>C-c</kbd><kbd>C-l</kbd> |
| `:CornelisGoals` | Show all goals | <kbd>C-c</kbd><kbd>C-?</kbd> |
| `:CornelisRestart` | Kill and restart the `agda` process | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-r</kbd> |
| `:CornelisAbort` | Abort running command | <kbd>C-c</kbd><kbd>C-x</kbd><kbd>C-a</kbd> |
| `:CornelisSolve <RW>` | Solve constraints | <kbd>C-c</kbd><kbd>C-s</kbd> |
| `:CornelisGoToDefinition` | Jump to definition of name at cursor | <kbd>M-.</kbd> or middle mouse button |
| `:CornelisPrevGoal` | Jump to previous goal | <kbd>C-c</kbd><kbd>C-b</kbd> |
| `:CornelisNextGoal` | Jump to next goal | <kbd>C-c</kbd><kbd>C-f</kbd> |
| `:CornelisQuestionToMeta` | Expand `?`-holes to `{! !}` | _(none)_ |
| `:CornelisInc` | Like `<C-A>` but also targets sub- and superscripts | _(none)_ |
| `:CornelisDec` | Like `<C-X>` but also targets sub- and superscripts | _(none)_ |
| `:CornelisCloseInfoWindows` | Close (all) info windows cornelis has opened | _(none)_ |

### Commands in context of a goal

Expand Down Expand Up @@ -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 <buffer> <leader>l :CornelisLoad<CR>
nnoremap <buffer> <leader>r :CornelisRefine<CR>
Expand Down
47 changes: 24 additions & 23 deletions src/Lib.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
5 changes: 4 additions & 1 deletion src/Plugin.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

0 comments on commit 9d83faa

Please sign in to comment.