Struct agda_mode::agda::ReplState

pub struct ReplState {
    pub stdin: ChildStdin,
    pub agda: AgdaRead,
    pub file: String,
    // some fields omitted
}

Simple REPL state wrapper.

Fields

stdin: ChildStdin

agda: AgdaRead

file: String

Implementations

impl ReplState

pub async fn response<'_>(&'_ mut self) -> Result<Resp>

Await the next Agda response.

impl ReplState

pub fn print_goal_list(&self)

Print all goals.

pub async fn reload_file<'_>(&'_ mut self) -> Result<()>

pub async fn command<'_>(&'_ mut self, cmd: Cmd) -> Result<()>

pub async fn command_raw<'_, '_>(
    &'_ mut self,
    raw_command: &'_ str
) -> Result<()>

pub async fn shutdown<'_>(&'_ mut self) -> Result<()>

pub async fn next_display_info<'_>(&'_ mut self) -> Result<DisplayInfo>

Skip information until the next display info.

pub fn interaction_points(&self) -> &[InteractionPoint]

Returns the latest next_goals result.

pub async fn next_goals<'_>(&'_ mut self) -> Result<()>

Skip information until the next interaction point (goal) list. The result can be queried via interaction_points.

Note

This information normally comes right after all_goals_warnings, and when you call next_all_goals_warnings, you've already eliminated errors. Therefore this method don't deal with errors.

pub async fn next_error<'_>(&'_ mut self) -> Result<AgdaError>

Skip information until an error.

impl ReplState

pub async fn next_give_action<'_>(&'_ mut self) -> NextResult<GiveAction>

impl ReplState

pub async fn next_make_case<'_>(&'_ mut self) -> NextResult<MakeCase>

impl ReplState

pub async fn next_highlight<'_>(&'_ mut self) -> NextResult<HighlightingInfo>

impl ReplState

pub async fn next_all_goals_warnings<'_>(
    &'_ mut self
) -> NextResult<AllGoalsWarnings>

impl ReplState

pub async fn next_goal_specific<'_>(&'_ mut self) -> NextResult<GoalSpecific>

impl ReplState

pub async fn next_module_contents<'_>(
    &'_ mut self
) -> NextResult<ModuleContents>

impl ReplState

pub async fn next_normal_form<'_>(&'_ mut self) -> NextResult<NormalForm>

impl ReplState

pub async fn next_context<'_>(&'_ mut self) -> NextResult<Context>

impl ReplState

pub async fn next_inferred_type<'_>(&'_ mut self) -> NextResult<InferredType>

impl ReplState

pub async fn validate_version_panicking<'_>(&'_ mut self)

pub async fn validate_version<'_>(&'_ mut self) -> Result<()>

Validate this Agda repl.

impl ReplState

pub async fn start<'_>(agda_program: &'_ str, file: String) -> Result<Self>

pub async fn from_io(
    stdin: ChildStdin,
    stdout: BufReader<ChildStdout>,
    file: String
) -> Result<Self>