Plugin

Documentation

runInteraction :: Interaction -> Neovim CornelisEnv ()

getDefinitionSites :: Buffer -> AgdaPos -> Neovim CornelisEnv (First DefinitionSite)

doGotoDefinition :: CommandArguments -> Neovim CornelisEnv ()

gotoDefinition :: Neovim CornelisEnv ()

doLoad :: CommandArguments -> Neovim CornelisEnv ()

atomicSwapIORef :: IORef a -> a -> IO a

load :: Neovim CornelisEnv ()

questionToMeta :: Buffer -> Neovim CornelisEnv ()

doAllGoals :: CommandArguments -> Neovim CornelisEnv ()

allGoals :: Neovim CornelisEnv ()

doRestart :: CommandArguments -> Neovim CornelisEnv ()

doAbort :: CommandArguments -> Neovim CornelisEnv ()

normalizationMode :: Neovim env Rewrite

computeMode :: Neovim env ComputeMode

solveOne :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

autoOne :: CommandArguments -> Neovim CornelisEnv ()

withNormalizationMode :: Maybe String -> (Rewrite -> Neovim e ()) -> Neovim e ()

withComputeMode :: Maybe String -> (ComputeMode -> Neovim e ()) -> Neovim e ()

typeContext :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

typeContextInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

doRefine :: CommandArguments -> Neovim CornelisEnv ()

refine :: Neovim CornelisEnv ()

doGive :: CommandArguments -> Neovim CornelisEnv ()

give :: Neovim CornelisEnv ()

doElaborate :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

elaborate :: Rewrite -> Neovim CornelisEnv ()

doTypeInfer :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

inferType :: Rewrite -> Neovim CornelisEnv ()

doWhyInScope :: CommandArguments -> Neovim CornelisEnv ()

whyInScope :: Text -> Neovim CornelisEnv ()

doNormalize :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

helperFunc :: Rewrite -> Text -> Neovim CornelisEnv ()

doHelperFunc :: CommandArguments -> Maybe String -> Neovim CornelisEnv ()

doCaseSplit :: CommandArguments -> Neovim CornelisEnv ()

caseSplit :: Text -> Neovim CornelisEnv ()

doQuestionToMeta :: CommandArguments -> Neovim CornelisEnv ()

goalWindow :: Buffer -> DisplayInfo -> Neovim CornelisEnv ()

computeModeCompletion :: String -> String -> Int -> Neovim env String

rewriteModeCompletion :: String -> String -> Int -> Neovim env String

debugCommandCompletion :: String -> String -> Int -> Neovim env String

doDebug :: CommandArguments -> String -> Neovim CornelisEnv ()

notifyEdit

Arguments

:: Text

the string "bytes"

-> BufferNum

buffer handle

-> Bool

b:changedtick

-> Int

start row of the changed text (zero-indexed)

-> Int

start column of the changed text

-> Int

byte offset of the changed text (from the start of the buffer)

-> Int

old end row of the changed text (relative to the start row)

-> Int

old end column of the changed text

-> Int

old end byte length of the changed text

-> Int

new end row of the changed text (relative to the start row)

-> Int

new end column of the changed text

-> Int

new end byte length of the changed text

-> Neovim CornelisEnv Bool

Return True to detach

The on_bytes callback required by nvim_buf_attach.

doCloseInfoWindows :: CommandArguments -> Neovim CornelisEnv ()