[−][src]Enum agda_mode::resp::DisplayInfo

pub enum DisplayInfo {
    CompilationOk {
        warnings: String,
        errors: String,
    },
    Constraints {
        constraints: Vec<OutputForm>,
    },
    AllGoalsWarnings(AllGoalsWarnings),
    Time {
        time: String,
    },
    Error(AgdaError),
    IntroNotFound,
    IntroConstructorUnknown {
        constructors: Vec<String>,
    },
    Auto {
        info: String,
    },
    ModuleContents(ModuleContents),
    SearchAbout {
        search: String,
        results: Vec<NamedPrettyTCM>,
    },
    WhyInScope {
        thing: String,
        filepath: String,
        message: String,
    },
    NormalForm(NormalForm),
    InferredType(InferredType),
    Context(Context),
    Version {
        version: String,
    },
    GoalSpecific(GoalSpecific),
}

Something that is displayed in the Emacs mode, serialized with more details.

Variants

CompilationOk

Fields of CompilationOk

warnings: Stringerrors: String

Constraints

Fields of Constraints

constraints: Vec<OutputForm>

AllGoalsWarnings(AllGoalsWarnings)

Time

Fields of Time

time: String

Error(AgdaError)

IntroNotFound

IntroConstructorUnknown

Fields of IntroConstructorUnknown

constructors: Vec<String>

Available constructors

Auto

Fields of Auto

info: String

ModuleContents(ModuleContents)

SearchAbout

Fields of SearchAbout

search: Stringresults: Vec<NamedPrettyTCM>

WhyInScope

Fields of WhyInScope

thing: Stringfilepath: Stringmessage: String

NormalForm(NormalForm)

InferredType(InferredType)

Context(Context)

Version

Fields of Version

version: String

GoalSpecific(GoalSpecific)

Trait Implementations

`impl Clone for DisplayInfo`[src]

`pub fn clone(&self) -> DisplayInfo`[src]

`pub fn clone_from(&mut self, source: &Self)`1.0.0[src]

`impl Debug for DisplayInfo`[src]

`pub fn fmt(&self, f: &mut Formatter<'_>) -> Result`[src]

`impl<'de> Deserialize<'de> for DisplayInfo`[src]

`pub fn deserialize<D>(deserializer: D) -> Result<Self, D::Error> where __D: Deserializer<'de>,` [src]

`impl Eq for DisplayInfo`[src]

`impl PartialEq<DisplayInfo> for DisplayInfo`[src]

`pub fn eq(&self, other: &DisplayInfo) -> bool`[src]

`pub fn ne(&self, other: &DisplayInfo) -> bool`[src]

`impl StructuralEq for DisplayInfo`[src]

`impl StructuralPartialEq for DisplayInfo`[src]

Auto Trait Implementations

`impl RefUnwindSafe for DisplayInfo`

`impl Send for DisplayInfo`

`impl Sync for DisplayInfo`

`impl Unpin for DisplayInfo`

`impl UnwindSafe for DisplayInfo`

Blanket Implementations

`impl<T> Any for T where T: 'static + ?Sized,` [src]

`pub fn type_id(&self) -> TypeId`[src]

`impl<T> Borrow<T> for T where T: ?Sized,` [src]

`pub fn borrow(&self) -> &T`[src]

`impl<T> BorrowMut<T> for T where T: ?Sized,` [src]

`pub fn borrow_mut(&mut self) -> &mut T`[src]

`impl<T> DeserializeOwned for T where T: for<'de> Deserialize<'de>,` [src]

`impl<T> From<T> for T`[src]

`pub fn from(t: T) -> T`[src]

`impl<T, U> Into for T where U: From<T>,` [src]

`pub fn into(self) -> U`[src]

`impl<T> ToOwned for T where T: Clone,` [src]

`type Owned = T`

The resulting type after obtaining ownership.

`pub fn to_owned(&self) -> T`[src]

`pub fn clone_into(&self, target: &mut T)`[src]

`impl<T, U> TryFrom for T where U: Into<T>,` [src]

`type Error = Infallible`

The type returned in the event of a conversion error.

`pub fn try_from(value: U) -> Result<T, <T as TryFrom>::Error>`[src]

`impl<T, U> TryInto for T where U: TryFrom<T>,` [src]

`type Error = >::Error`

The type returned in the event of a conversion error.

[−][src]Enum agda_mode::resp::DisplayInfo

Variants

Fields of CompilationOk

Fields of Constraints

Fields of Time

Fields of IntroConstructorUnknown

Fields of Auto

Fields of SearchAbout

Fields of WhyInScope

Fields of Version

Trait Implementations

impl Clone for DisplayInfo[src]

pub fn clone(&self) -> DisplayInfo[src]

pub fn clone_from(&mut self, source: &Self)1.0.0[src]

impl Debug for DisplayInfo[src]

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

impl<'de> Deserialize<'de> for DisplayInfo[src]

pub fn deserialize<__D>(__deserializer: __D) -> Result<Self, __D::Error> where __D: Deserializer<'de>, [src]

impl Eq for DisplayInfo[src]

impl PartialEq<DisplayInfo> for DisplayInfo[src]

pub fn eq(&self, other: &DisplayInfo) -> bool[src]

pub fn ne(&self, other: &DisplayInfo) -> bool[src]

impl StructuralEq for DisplayInfo[src]

impl StructuralPartialEq for DisplayInfo[src]

Auto Trait Implementations

impl RefUnwindSafe for DisplayInfo

impl Send for DisplayInfo

impl Sync for DisplayInfo

impl Unpin for DisplayInfo

impl UnwindSafe for DisplayInfo

Blanket Implementations

impl<T> Any for T where T: 'static + ?Sized, [src]

pub fn type_id(&self) -> TypeId[src]

impl<T> Borrow<T> for T where T: ?Sized, [src]

pub fn borrow(&self) -> &T[src]

impl<T> BorrowMut<T> for T where T: ?Sized, [src]

pub fn borrow_mut(&mut self) -> &mut T[src]

impl<T> DeserializeOwned for T where T: for<'de> Deserialize<'de>, [src]

impl<T> From<T> for T[src]

pub fn from(t: T) -> T[src]

impl<T, U> Into<U> for T where U: From<T>, [src]

pub fn into(self) -> U[src]

impl<T> ToOwned for T where T: Clone, [src]

type Owned = T

pub fn to_owned(&self) -> T[src]

pub fn clone_into(&self, target: &mut T)[src]

impl<T, U> TryFrom<U> for T where U: Into<T>, [src]

type Error = Infallible

pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>[src]

impl<T, U> TryInto<U> for T where U: TryFrom<T>, [src]

type Error = <U as TryFrom<T>>::Error

pub fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>[src]