agda_mode/resp/
hl.rs

1use crate::base::TokenBased;
2use crate::pos::IntPos;
3use either::Either;
4use serde::Deserialize;
5
6/// A token highlighting information.
7/// The token is somehow called `Aspect` in Agda.
8#[serde(rename_all = "camelCase")]
9#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
10pub struct AspectHighlight {
11    pub range: (IntPos, IntPos),
12    pub atoms: Vec<String>,
13    pub token_based: TokenBased,
14    pub note: Option<String>,
15    pub definition_site: Option<DefinitionSite>,
16}
17
18/// Jump to library definition information.
19#[serde(rename_all = "camelCase")]
20#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
21pub struct DefinitionSite {
22    pub filepath: String,
23    pub position: IntPos,
24}
25
26/// A list of token highlighting information.
27#[serde(rename_all = "camelCase")]
28#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
29pub struct Highlighting {
30    pub remove: bool,
31    pub payload: Vec<AspectHighlight>,
32}
33
34#[serde(rename_all = "camelCase")]
35#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq)]
36pub struct HighlightingInfo {
37    info: Option<Highlighting>,
38    filepath: Option<String>,
39    direct: bool,
40}
41
42impl HighlightingInfo {
43    pub fn into_either(self) -> Either<Highlighting, String> {
44        if self.direct {
45            debug_assert!(self.filepath.is_none());
46            Either::Left(self.info.unwrap())
47        } else {
48            debug_assert!(self.info.is_none());
49            Either::Right(self.filepath.unwrap())
50        }
51    }
52}
agda_mode/resp/hl.rs

agda_mode/resp/
hl.rs
