Enum agda_mode::resp::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 of Status

status: Status

JumpToError

Fields of JumpToError

filepath: Stringposition: i32

InteractionPoints

Fields of InteractionPoints

interaction_points: Vec<InteractionPoint>

GiveAction(GiveAction)

MakeCase(MakeCase)

Response is list of printed clauses.

SolveAll

Solution for one or more meta-variables.

Fields of SolveAll

solutions: Vec<OneSolution>

DisplayInfo

Fields of DisplayInfo

info: Option<DisplayInfo>

RunningInfo

The integer is the message's debug level.

Fields of RunningInfo

debug_level: i32message: String

ClearRunningInfo

ClearHighlighting

Clear highlighting of the given kind.

Fields of ClearHighlighting

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 copy of the value.

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

Performs copy-assignment from source.

impl Eq for Resp

impl PartialEq<Resp> for Resp

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

This method tests for self and other values to be equal, and is used by ==.

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

This method tests for !=.

impl Debug for Resp

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

Formats the value using the given formatter.

impl StructuralPartialEq for Resp

impl StructuralEq for Resp

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.