Get-persistent-whs
Make a wormhole's status visible outside the wormhole
General Form:
(get-persistent-whs name state)
Name should be the name of a wormhole (see wormhole). This
function returns an error-triple of the form (mv nil s state),
where s is the persistent-whs of the named wormhole (i.e., the status of
of wormhole stored outside of the ACL2 state). The status is obtained by
reading the oracle in the ACL2 state with read-ACL2-oracle.
Recall that the status of a wormhole is some ACL2 object largely determined
by the author of the wormhole. It is always treated as a pair whose car
is the “entry code” (:enter or :skip) or, more
precisely, is either :skip or not :skip, the latter case being
treated like :enter. But the cdr of the status can be whatever the
author of the wormhole chooses to hold the data of the wormhole. When a
wormhole is entered its persistent status, aka its persistent-whs, is used to
configure the state of the read-eval-print loop the user sees inside the
wormhole. In particular, upon entry the persistent-whs is moved to the value
of the state global variable 'wormhole-status and is thus accessible via
(f-get-global 'wormhole-status state). We call this copy of the status
the ephemeral-whs because when the wormhole is exited the ephemeral-whs is
moved to the persistent-whs and the state global 'wormhole-status
is restored to whatever value it had when the wormhole was entered.
See wormhole-status for a discussion of these two senses of the
status of a wormhole. See also wormhole-programming-tips.
