Struct LeanCallbackHandle 

pub struct LeanCallbackHandle<P: LeanCallbackPayload> { /* private fields */ }

RAII registration for a Rust callback Lean may invoke.

Register with a supported payload specialization, pass LeanCallbackHandle::abi_parts to a Lean export whose first two arguments are USize, and keep the handle alive until the Lean side cannot call it again. Dropping the handle unregisters its id; a later Lean call with the same stale id returns LeanCallbackStatus::StaleHandle instead of dereferencing freed Rust memory.

The callback runs synchronously on the Lean-bound thread that invoked the Lean export. It must not call back into the same LeanSession or re-enter the same Lean call stack. Rust panics are caught inside the trampoline and recorded as LeanError with crate::HostStage::CallbackPanic; aborting panics and Lean internal panics remain process-scoped.

LeanCallbackHandle is Send and Sync because registry lookup clones an internal Arc before running the callback, and registration/removal is guarded by a mutex. The registered closure must therefore be Send + Sync + 'static.

Implementations

impl LeanCallbackHandle<LeanProgressTick>

pub fn register<F>(callback: F) -> LeanResult<Self>

where F: Fn(LeanProgressTick) -> LeanCallbackFlow + Send + Sync + 'static,

Register a Rust callback for progress tick payloads.

Errors

Returns LeanError::Host with diagnostic code crate::LeanDiagnosticCode::Internal if the registry cannot allocate a fresh nonzero id. This requires exhausting the process-size usize id space while many handles are still live.

impl LeanCallbackHandle<LeanStringEvent>

pub fn register<F>(callback: F) -> LeanResult<Self>

where F: Fn(LeanStringEvent) -> LeanCallbackFlow + Send + Sync + 'static,

Register a Rust callback for string payloads.

The Lean string is copied into an owned String before user code runs, so no Lean object lifetime escapes the trampoline.

Errors

Returns LeanError::Host with diagnostic code crate::LeanDiagnosticCode::Internal if the registry cannot allocate a fresh nonzero id.

impl<P: LeanCallbackPayload> LeanCallbackHandle<P>

pub fn abi_handle(&self) -> usize

Opaque USize handle to pass as the first Lean callback argument.

pub fn abi_trampoline(&self) -> usize

Crate-owned trampoline value to pass as the second Lean callback argument.

Callers may pass this value to Lean, but they never construct or supply a trampoline function pointer themselves.

pub fn abi_parts(&self) -> (usize, usize)

Return (handle, trampoline) for Lean exports using the standard two-USize callback ABI.

pub fn last_error(&self) -> Option<LeanError>

Last Rust error recorded by this callback handle.

This is currently populated when the callback panics and the trampoline returns LeanCallbackStatus::Panic. Stale-handle calls happen after the handle was dropped, so no live handle exists to store that status.

Trait Implementations

impl<P: LeanCallbackPayload> Debug for LeanCallbackHandle<P>

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

Formats the value using the given formatter.

impl<P: LeanCallbackPayload> Drop for LeanCallbackHandle<P>

fn drop(&mut self)

Executes the destructor for this type.

fn pin_drop(self: Pin<&mut Self>)

🔬This is a nightly-only experimental API. (pin_ergonomics)

Execute the destructor for this type, but different to Drop::drop, it requires self to be pinned.