Enum Resp 

pub enum Resp {
    HighlightingInfo(HighlightingInfo),
    Status {
        status: Status,
    },
    JumpToError {
        filepath: String,
        position: i32,
    },
    InteractionPoints {
        interaction_points: Vec<InteractionPoint>,
    },
    GiveAction(GiveAction),
    MakeCase(MakeCase),
    SolveAll {
        solutions: Vec<OneSolution>,
    },
    DisplayInfo {
        info: Option<DisplayInfo>,
    },
    RunningInfo {
        debug_level: i32,
        message: String,
    },
    ClearRunningInfo,
    ClearHighlighting {
        token_based: TokenBased,
    },
    DoneAborting,
}

Agda response.

Variants

HighlightingInfo(HighlightingInfo)

Status

Fields

status: Status

JumpToError

Fields

filepath: String

position: i32

InteractionPoints

Fields

interaction_points: Vec<InteractionPoint>

GiveAction(GiveAction)

MakeCase(MakeCase)

Response is list of printed clauses.

SolveAll

Solution for one or more meta-variables.

Fields

solutions: Vec<OneSolution>

DisplayInfo

Fields

info: Option<DisplayInfo>

RunningInfo

The integer is the message’s debug level.

Fields

debug_level: i32

message: String

ClearRunningInfo

ClearHighlighting

Clear highlighting of the given kind.

Fields

token_based: TokenBased

DoneAborting

A command sent when an abort command has completed successfully.

Trait Implementations

impl Clone for Resp

fn clone(&self) -> Resp

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Resp

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for Resp

fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl PartialEq for Resp

fn eq(&self, other: &Resp) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Resp

impl StructuralPartialEq for Resp