		Search-engine friendly clone of the ACL2 documentation.

User-interface

Manage-screen-output

Manage the screen output generated from an event form.

Signature
(manage-screen-output verbose form) → form-with-output-managed
Arguments: form — Guard (pseudo-event-formp form).
Returns: form-with-output-managed — Type (pseudo-event-formp form-with-output-managed), given the guard.

If verbose is not nil or 'nil, keep all screen output. If verbose is nil or 'nil, suppress all non-error screen output.

This function can be used in a macro of the following form:

(defmacro mac (... &key verbose ...)
  (manage-screen-output verbose `(make-event ...)))

Invoking mac at the ACL2 top-level will submit the event, with the screen output managed by verbose.

Note that if form is an event (see embedded-event-form), then (manage-screen-output verbose form) evaluates to an event.

Definitions and Theorems

Function: manage-screen-output

(defun manage-screen-output (verbose form)
  (declare (xargs :guard (pseudo-event-formp form)))
  (let ((__function__ 'manage-screen-output))
    (declare (ignorable __function__))
    (manage-screen-output-aux verbose form nil)))

Theorem: pseudo-event-formp-of-manage-screen-output

(defthm pseudo-event-formp-of-manage-screen-output
 (implies
   (and (pseudo-event-formp form))
   (b*
    ((form-with-output-managed (manage-screen-output verbose form)))
    (pseudo-event-formp form-with-output-managed)))
 :rule-classes :rewrite)