agda_mode/resp/
give.rs

1use crate::pos::InteractionPoint;
2use either::Either;
3use serde::Deserialize;
4
5/// Give action result
6///
7/// Comment derived from agda2-mode.el
8///
9/// If 'GiveResult' is 'Give_String s', then the goal is replaced by 's',
10/// and otherwise the text inside the goal is retained (parenthesised
11/// if 'GiveResult' is 'Give_Paren').
12#[serde(rename_all = "camelCase")]
13#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
14pub struct GiveResult {
15    str: Option<String>,
16    paren: Option<bool>,
17}
18
19impl GiveResult {
20    pub fn into_either(self) -> Either<String, bool> {
21        match (self.str, self.paren) {
22            (Some(s), None) => Either::Left(s),
23            (None, Some(b)) => Either::Right(b),
24            _ => unreachable!(),
25        }
26    }
27}
28
29#[serde(rename_all = "camelCase")]
30#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
31pub struct GiveAction {
32    pub give_result: GiveResult,
33    pub interaction_point: InteractionPoint,
34}
agda_mode/resp/give.rs

agda_mode/resp/
give.rs
