Interactive_snapshot (imandra-base.Imandra_interactive.Interactive

Snapshot of all of Interactive

This module controls the state of most of Imandra_interactive. It allows push/pop control of the state, for transactions, and named snapshots for #undo directives or other forms of explicit state checkout.

Snapshot for Globals_.event_state_

include Imandra_util.Snapshot_sigs.S

val push : scope:Opentelemetry.Trace.scope option -> unit -> unit

val pop_restore : scope:Opentelemetry.Trace.scope option -> unit -> unit

val pop_delete : scope:Opentelemetry.Trace.scope option -> unit -> unit

val is_empty : unit -> bool

val with_push : 
  scope:Opentelemetry.Trace.scope option ->
  restore_if_ok:bool ->
  ( unit -> 'a ) ->
  'a

val save_named : scope:Opentelemetry.Trace.scope option -> int -> unit

val restore_named : scope:Opentelemetry.Trace.scope option -> int -> unit

val delete_named : scope:Opentelemetry.Trace.scope option -> int -> unit

val pp_named_debug : int CCFormat.printer

module Gen_snap : sig ... end

Generation of snapshots with unique names