		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Restore-output

Wrap an event form to have it produce screen output according to previously saved screen output settings.

Signature
(restore-output event) → new-event
Arguments: event — Guard (pseudo-event-formp event).
Returns: new-event — Type (pseudo-event-formp new-event).

This wraps the form in a (with-output :stack :pop ...). Among other possible uses, this can be used on a sub-form of the form passed to a make-event-terse.

Definitions and Theorems

Function: restore-output

(defun restore-output (event)
       (declare (xargs :guard (pseudo-event-formp event)))
       (let ((__function__ 'restore-output))
            (declare (ignorable __function__))
            (cons 'with-output
                  (cons ':stack
                        (cons ':pop (cons event 'nil))))))

Theorem: pseudo-event-formp-of-restore-output

(defthm pseudo-event-formp-of-restore-output
        (b* ((new-event (restore-output event)))
            (pseudo-event-formp new-event))
        :rule-classes :rewrite)