|
|
|---|
|
|
|
|---|
Hooks that fire when the ACL2s interface quiet mode is turned on or off.
General form(add-quiet-mode-on-hook
name ; A (symbol) name to associate with this hook
hook) ; A function to call when quiet mode transitions from disabled to enabled.
; The return value of the hook function should be a list of ACL2 forms to
; be executed.
(add-quiet-mode-off-hook
name ; A (symbol) name to associate with this hook
hook) ; A function to call when quiet mode transitions from enabled to disabled.
; The return value of the hook function should be a list of ACL2 forms to
; be executed.
Some applications may have verbosity settings beyond the standard ACL2 ones. Quiet mode hooks provide a way to change these settings whenever the ACL2s interface transitions from quiet mode being enabled to disabled, and vice versa.
Upon the appropriate transition, each hook function for that transition is called.
The return values of all of the hook functions for that transition type are
appended, and the resulting list of ACL2 forms is evaluated using ACL2::ld
in an environment that disables all output. Typically, hooks will perform some
stateful operation (for example, a quiet-mode-on hook might save the current value
of a setting into a variable) and then produce a list of ACL2 forms that will change
the setting to its original value (for a quiet-mode-off hook) or to a particular
quiet value (for a quiet-mode-on hook). One should not call any of
For each transition type, adding a hook with the same name as another hook for that same transition type will result in the previously added hook being removed from the list of hooks.
Examples;; Define a variable to store the last seen gag mode. ;; See books/acl2s/interface/acl2s-interface.lsp for the definition ;; of define-var, which is needed to work around SBCL and CCL quirks. (define-var *saved-gag-mode* (acl2::gag-mode)) (add-quiet-mode-on-hook :gag-mode (lambda () ;; Calling acl2::@ here is probably not super safe, but it seems to work... (setf *saved-gag-mode* (acl2::@ acl2::gag-mode)) '((acl2::set-gag-mode t)))) (add-quiet-mode-off-hook :gag-mode (lambda () `((acl2::set-gag-mode ,*saved-gag-mode*))))
See