summaryrefslogtreecommitdiff
path: root/isabelle-proto/src/pipe.rs
blob: ef80ff33b5ab22dab6bb847805e316626f287dd5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
use regex::Regex;
use serde::Deserialize;
use std::{io::{BufRead, BufReader}, process::ChildStdout};

use crate::messages::*;

pub(crate) fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
where T: Deserialize<'a> {
    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
    let mat = regex.find(msg)?;
    let ty = &msg[..mat.end()];
    let rest = &msg[mat.end()..];

    match ty {
        "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
        "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
        _ => None
    }
}

pub(crate) fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
    let mat = regex.find(msg)?;
    let ty = &msg[..mat.end()];
    let rest = &msg[mat.end()..];

    match ty {
        "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
        "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
        "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
        _ => None
    }
}




pub(crate) fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
    for res in pipe.lines() {
        match res {
            Err(_) => (),
            Ok(line) => {
                let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
                if let Some(SyncAnswer::Ok(data)) = hello {
                    return Some(data);
                }
            }
        }
    }
    None
}


pub(crate) fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
    let mut res = String::new();
    reader.read_line(&mut res).unwrap();
    match decode_sync(&res).unwrap() {
        SyncAnswer::Ok(AsyncStartOk { task }) => task,
        SyncAnswer::Error(_) => panic!("failed to start async task!")
    }
}