		Search-engine friendly clone of the ACL2 documentation.

User-interface

Control-screen-output

Control the screen output generated from an event form.

Signature
(control-screen-output verbose form) → form-with-output-controlled
Arguments: form — Guard (pseudo-event-formp form).
Returns: form-with-output-controlled — Type (pseudo-event-formp form-with-output-controlled), 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 ...)
  (control-screen-output verbose `(make-event ...)))

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

Definitions and Theorems

Function: control-screen-output

(defun control-screen-output (verbose form)
 (declare (xargs :guard (pseudo-event-formp form)))
 (let ((__function__ 'control-screen-output))
  (declare (ignorable __function__))
  (cond
   ((maybe-unquote verbose) form)
   (t
    (cons
     'with-output
     (cons
      ':gag-mode
      (cons
          'nil
          (cons ':off
                (cons ':all
                      (cons ':on
                            (cons 'error (cons form 'nil))))))))))))

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

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