agda_mode/agda/
read.rs

1use std::io;
2
3use serde::Deserialize;
4use tokio::io::{AsyncBufReadExt, BufReader};
5use tokio::process::ChildStdout;
6
7use crate::agda::ReplState;
8use crate::debug::debug_response;
9use crate::resp::Resp;
10
11/// Deserialize from Agda's command line output.
12pub fn deserialize_agda<'a, T: Deserialize<'a>>(buf: &'a str) -> serde_json::Result<T> {
13    let buf = buf.trim_start_matches("JSON>").trim();
14    serde_json::from_str(buf)
15}
16
17pub struct AgdaRead {
18    buf: String,
19    agda: BufReader<ChildStdout>,
20}
21
22impl From<BufReader<ChildStdout>> for AgdaRead {
23    fn from(agda: BufReader<ChildStdout>) -> Self {
24        Self {
25            agda,
26            buf: String::with_capacity(2048),
27        }
28    }
29}
30
31impl From<ChildStdout> for AgdaRead {
32    fn from(o: ChildStdout) -> Self {
33        From::from(BufReader::new(o))
34    }
35}
36
37impl AgdaRead {
38    /// Take Agda's response from the next line.
39    pub async fn response(&mut self) -> io::Result<Resp> {
40        self.agda.read_line(&mut self.buf).await?;
41        unsafe { debug_response(format!("[RES]: {}\n", self.buf)) };
42        let resp = deserialize_agda(&self.buf)?;
43        self.buf.clear();
44        Ok(resp)
45    }
46}
47
48impl ReplState {
49    /// Await the next Agda response.
50    pub async fn response(&mut self) -> io::Result<Resp> {
51        self.agda.response().await
52    }
53}
agda_mode/agda/read.rs

agda_mode/agda/
read.rs
