agda-mode 0.1.8

Accessing Agda's interaction mode via command line, in Rust
Documentation 
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

use crate::base::TokenBased;
use crate::pos::IntPos;
use either::Either;
use serde::Deserialize;

/// A token highlighting information.
/// The token is somehow called `Aspect` in Agda.
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct AspectHighlight {
    pub range: (IntPos, IntPos),
    pub atoms: Vec<String>,
    pub token_based: TokenBased,
    pub note: Option<String>,
    pub definition_site: Option<DefinitionSite>,
}

/// Jump to library definition information.
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct DefinitionSite {
    pub filepath: String,
    pub position: IntPos,
}

/// A list of token highlighting information.
#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct Highlighting {
    pub remove: bool,
    pub payload: Vec<AspectHighlight>,
}

#[serde(rename_all = "camelCase")]
#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
pub struct HighlightingInfo {
    info: Option<Highlighting>,
    filepath: Option<String>,
    direct: bool,
}

impl HighlightingInfo {
    pub fn into_either(self) -> Either<Highlighting, String> {
        if self.direct {
            debug_assert!(self.filepath.is_none());
            Either::Left(self.info.unwrap())
        } else {
            debug_assert!(self.info.is_none());
            Either::Right(self.filepath.unwrap())
        }
    }
}