Cornelis.Goals

Documentation

getIpInterval :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv AgdaInterval

Get the spanning interval of an interaction point. If we already have highlighting information from vim, use the extmark for this goal, otherwise using the interval that Agda knows about.

findGoal :: Ord a => (AgdaPos -> AgdaPos -> Maybe a) -> Neovim CornelisEnv ()

Move the vim cursor to a goal in the current window

prevGoal :: Neovim CornelisEnv ()

Move the vim cursor to the previous interaction point.

nextGoal :: Neovim CornelisEnv ()

Move the vim cursor to the next interaction point.

getGoalAtCursor :: Neovim CornelisEnv (Buffer, Maybe (InteractionPoint Identity))

Uses highlighting extmarks to determine what a hole is; since the user might have typed inside of a {! !} goal since they last saved.

getGoalAtPos :: Buffer -> AgdaPos -> Neovim CornelisEnv (Maybe (InteractionPoint Identity))

withGoalAtCursor :: (Buffer -> InteractionPoint Identity -> Neovim CornelisEnv a) -> Neovim CornelisEnv (Maybe a)

Run a continuation on a goal at the current position in the current buffer, if it exists.

withGoalContentsOrPrompt

Arguments

:: String

Text to print when prompting the user for input

-> (InteractionPoint Identity -> String -> Neovim CornelisEnv a)

Continuation to run on goal, with hole contents

-> (String -> Neovim CornelisEnv a)

Continuation to run on user input if there's no goal here

-> Neovim CornelisEnv a

Run the first continuation on the goal at the current position, otherwise run the second continuation.

If there is a non-empty hole, provide its content to the first continuation. If the hole is empty, prompt for input and provide that.

If there is no goal, prompt the user for input and run the second continuation.

getGoalContentsMaybe :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv (Maybe Text)

Get the contents of a goal.

getGoalContents :: Buffer -> InteractionPoint Identity -> Neovim CornelisEnv Text

Like getGoalContents_maybe.

replaceQuestion :: Text -> Text

Replace all single ? tokens with interaction holes.