		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)