Cornelis.Agda

Documentation

debugJson :: Bool

When true, dump out received JSON as it arrives.

spawnAgda :: Buffer -> Neovim CornelisEnv Agda

Create an Agda environment for the given buffer. This spawns an asynchronous thread that keeps an agda process alive as long as vim is open.

TODO(sandy): This leaks the process when the buffer is closed.

dropPrefix :: Text -> Text -> Text

Drop a prefix from the text, if it exists.

runIOTCM :: Interaction -> Agda -> Neovim env ()

Send an Interaction to an Agda.

buildIOTCM :: Interaction -> Buffer -> Neovim env IOTCM

Construct an IOTCM for a buffer.

withCurrentBuffer :: (Buffer -> Neovim env a) -> Neovim env a

Get the current buffer and run the continuation.

withAgda :: Neovim CornelisEnv a -> Neovim CornelisEnv a

Ensure we have a BufferStuff attached to the current buffer.

getAgda :: Buffer -> Neovim CornelisEnv Agda

Get the Agda environment for a given buffer.