agda_mode/resp/
mod.rs

1use serde::Deserialize;
2
3use crate::base::TokenBased;
4use crate::pos::InteractionPoint;
5
6pub use self::di::*;
7pub use self::give::*;
8pub use self::goal::*;
9pub use self::hl::*;
10pub use self::oc::*;
11
12/// Display info.
13mod di;
14/// About the "Give" action.
15mod give;
16/// Goal information.
17mod goal;
18/// Highlighting.
19mod hl;
20/// Output constraints (user goals & unsolved metas).
21mod oc;
22
23#[serde(rename_all = "camelCase")]
24#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
25pub struct MakeCase {
26    pub variant: MakeCaseVariant,
27    pub interaction_point: InteractionPoint,
28    pub clauses: Vec<String>,
29}
30
31/// Status information.
32#[serde(rename_all = "camelCase")]
33#[derive(Deserialize, Clone, Default, Debug, Eq, PartialEq, Hash)]
34pub struct Status {
35    /// Are implicit arguments displayed?
36    pub show_implicit_arguments: bool,
37    /// Has the module been successfully type checked?
38    pub checked: bool,
39}
40
41#[derive(Deserialize, Copy, Clone, Debug, Eq, PartialEq, Hash)]
42pub enum MakeCaseVariant {
43    Function,
44    ExtendedLambda,
45}
46
47#[serde(rename_all = "camelCase")]
48#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
49pub struct OneSolution {
50    pub interaction_point: InteractionPoint,
51    pub expression: String,
52}
53
54/// Agda response.
55#[serde(tag = "kind")]
56#[derive(Deserialize, Clone, Debug, Eq, PartialEq)]
57pub enum Resp {
58    HighlightingInfo(HighlightingInfo),
59    Status {
60        status: Status,
61    },
62    JumpToError {
63        filepath: String,
64        position: i32,
65    },
66    InteractionPoints {
67        #[serde(rename = "interactionPoints")]
68        interaction_points: Vec<InteractionPoint>,
69    },
70    GiveAction(GiveAction),
71    /// Response is list of printed clauses.
72    MakeCase(MakeCase),
73    /// Solution for one or more meta-variables.
74    SolveAll {
75        solutions: Vec<OneSolution>,
76    },
77    DisplayInfo {
78        info: Option<DisplayInfo>,
79    },
80    /// The integer is the message's debug level.
81    RunningInfo {
82        #[serde(rename = "debugLevel")]
83        debug_level: i32,
84        message: String,
85    },
86    ClearRunningInfo,
87    /// Clear highlighting of the given kind.
88    ClearHighlighting {
89        #[serde(rename = "tokenBased")]
90        token_based: TokenBased,
91    },
92    /// A command sent when an abort command has completed successfully.
93    DoneAborting,
94}
agda_mode/resp/mod.rs

agda_mode/resp/
mod.rs
