Struct IsabelleClient

pub struct IsabelleClient { /* private fields */ }

Provides interaction with Isabelle servers.

Implementations

impl IsabelleClient

pub fn connect(address: Option<&str>, port: u32, pass: &str) -> Self

Connect to an Isabelle server.

Arguments

• address: specifies the server address. If it is None, “127.0.0.1” is use as a default
• port: specifies the server port
• pass: the password

pub fn for_server(server: &IsabelleServer) -> Self

Connect to an Isabelle server using the information from a IsabelleServer instance.

pub async fn echo( &mut self, echo: &str, ) -> Result<SyncResult<String, String>, Error>

Identity function: Returns its argument as result

pub async fn shutdown(&mut self) -> Result<SyncResult<(), String>, Error>

Forces a shut- down of the connected server process, stopping all open sessions and closing the server socket. This may disrupt pending commands on other connections.

pub async fn cancel( &mut self, task_id: String, ) -> Result<SyncResult<(), ()>, Error>

Attempts to cancel the specified task. Cancellation is merely a hint that the client prefers an ongoing process to be stopped.

pub async fn session_build( &mut self, args: &SessionBuildArgs, ) -> Result<AsyncResult<SessionBuildResults, SessionBuildResults>, Error>

Prepares a session image for interactive use of theories.

pub async fn session_start( &mut self, args: &SessionBuildArgs, ) -> Result<AsyncResult<SessionStartResult, ()>, Error>

Starts a new Isabelle/PIDE session with underlying Isabelle/ML process, based on a session image that it produces on demand using session_build. Returns the session_id, which provides the internal identification of the session object within the server process.

pub async fn session_stop( &mut self, args: &SessionStopArgs, ) -> Result<AsyncResult<SessionStopResult, SessionStopResult>, Error>

Forces a shutdown of the identified session.

pub async fn use_theories( &mut self, args: &UseTheoriesArgs, ) -> Result<AsyncResult<UseTheoryResults, ()>, Error>

Updates the identified session by adding the current version of theory files to it, while dependencies are resolved implicitly.

pub async fn purge_theories( &mut self, args: PurgeTheoryArgs, ) -> Result<SyncResult<PurgeTheoryResults, ()>, Error>

Updates the identified session by removing theories. Theories that are used in pending use_theories tasks or imported by other theories are retained.