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

use crate::pos::InteractionPoint;
use either::Either;
use serde::Deserialize;

/// Give action result
///
/// Comment derived from agda2-mode.el
///
/// If 'GiveResult' is 'Give_String s', then the goal is replaced by 's',
/// and otherwise the text inside the goal is retained (parenthesised
/// if 'GiveResult' is 'Give_Paren').
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct GiveResult {
    str: Option<String>,
    paren: Option<bool>,
}

impl GiveResult {
    pub fn into_either(self) -> Either<String, bool> {
        match (self.str, self.paren) {
            (Some(s), None) => Either::Left(s),
            (None, Some(b)) => Either::Right(b),
            _ => unreachable!(),
        }
    }
}

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct GiveAction {
    pub give_result: GiveResult,
    pub interaction_point: InteractionPoint,
}