[−][src]Crate agda_mode
Accessing Agda's interaction mode via command line. This library is created for agda-tac. It works with stable rust starting from 1.39.0.
This crate will work only with master-branch Agda until Agda 2.6.1 is released. Tracking issues for the feature are agda#4183 and agda#4209, both work for JSON now.
Basic usage
Invoke ReplState::start
and await the REPL to be available.
That's the wrapper of the Agda REPL's state.
Then you may:
+ Invoke ReplState::reload_file
to reload the current file
+ Invoke ReplState::command
to send a command to Agda
+ Invoke ReplState::response
to await for the next response from Agda.
+ Note that Agda sends json to agda-mode
.
The deserialized json type is Resp
.
There are more utilities to access Agda, checkout the library documentation to see all of them.
Implementation notes
This crate deserialize json via serde_json
,
and do async process io handling via tokio
.
Modules
agda | Invoke Agda in command line and interact with it via stdio. |
base | Common types (used in both input/output to Agda). |
cmd | Agda commands (input to Agda). |
debug | Debugging utilities. |
hs | Haskell interaction utilities. |
pos | Position types, used in both |
resp | Response data types (output of Agda). |