restore-output

(in-package "ACL2")

(define restore-output
  ((event pseudo-event-formp))
  :returns (new-event pseudo-event-formp)
  :parents (event-macros)
  :short "Wrap an event form to have it produce screen output
          according to previously saved screen output settings."
  :long (topstring-p "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 @(tsee make-event-terse).")
  `(with-output :stack :pop ,EVENT))

(define restore-output?
  ((yes/no booleanp) (event pseudo-event-formp))
  :returns (new-event pseudo-event-formp
    :hyp (pseudo-event-formp event)
    :hints (("Goal" :in-theory (disable pseudo-event-formp))))
  :parents (event-macros)
  :short "Conditionally wrap an event form to have it produce screen output
          according to previously saved screen output settings."
  :long (topstring-p "This leaves the form unchanged if the boolean is @('nil'),
    otherwise it calls @(tsee restore-output) on it.")
  (if yes/no
    (restore-output event)
    event))