agda_mode/
lib.rs

1/*!
2Accessing Agda's interaction mode via command line.
3This library is created for [agda-tac](https://lib.rs/agda-tac).
4It works with stable rust starting from 1.39.0.
5
6 [agda#4183]: https://github.com/agda/agda/issues/4183
7 [agda#4209]: https://github.com/agda/agda/issues/4209
8
9This crate will work only with master-branch Agda until Agda 2.6.1 is released.
10Tracking issues for the feature are [agda#4183] and [agda#4209], both work for JSON now.
11
12## Basic usage
13
14Invoke [`ReplState::start`](crate::agda::ReplState::start) and await the REPL to be available.
15That's the wrapper of the Agda REPL's state.
16
17Then you may:
18+ Invoke [`ReplState::reload_file`](crate::agda::ReplState::reload_file) to reload the current file
19+ Invoke [`ReplState::command`](crate::agda::ReplState::command) to send a command to Agda
20+ Invoke [`ReplState::response`](crate::agda::ReplState::response)
21  to await for the next response from Agda.
22  + Note that Agda sends json to `agda-mode`.
23    The deserialized json type is [`Resp`](crate::resp::Resp).
24
25There are more utilities to access Agda, checkout the library documentation to see all of them.
26
27## Implementation notes
28
29This crate deserialize json via `serde_json`,
30and do async process io handling via `tokio`.
31*/
32
33/// Haskell interaction utilities.
34pub mod hs;
35
36/// Common types (used in both input/output to Agda).
37pub mod base;
38
39/// Debugging utilities.
40pub mod debug;
41
42/// Position types, used in both `resp` & `cmd`.
43pub mod pos;
44
45/// Response data types (output of Agda).
46pub mod resp;
47
48/// Agda commands (input to Agda).
49pub mod cmd;
50
51/// Invoke Agda in command line and interact with it via stdio.
52pub mod agda;
agda_mode/lib.rs

agda_mode/
lib.rs
