Struct ReplState 

pub struct ReplState {
    pub stdin: ChildStdin,
    pub agda: AgdaRead,
    pub file: String,
    /* private fields */
}

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>