Struct agda_mode::cmd::IOTCM

pub struct IOTCM {
    pub command: Cmd,
    // some fields omitted
}

Fields

command: Cmd

Implementations

impl IOTCM

pub fn new(
    level: HighlightingLevel,
    file: String,
    method: HighlightingMethod,
    command: Cmd
) -> Self

pub fn simple(file: String, command: Cmd) -> Self

pub fn to_string(&self) -> String

Convert self into a command string.

Trait Implementations

impl Clone for IOTCM

pub fn clone(&self) -> IOTCM

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for IOTCM

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

Formats the value using the given formatter.

impl Display for IOTCM

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

Formats the value using the given formatter.