• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • Std/util
      • Apt
      • Defdata
      • Defrstobj
      • Seq
      • Match-tree
      • Defrstobj
      • With-supporters
      • Def-partial-measure
      • Template-subst
      • Soft
      • Defthm-domain
      • Event-macros
        • Evmac-input-hints-p
        • Function-definedness
        • Event-macro-input-processing
        • Event-macro-screen-printing
        • Evmac-input-print-p
        • Make-event-terse
          • Event-macro-applicability-conditions
          • Event-macro-results
          • Template-generators
          • Event-macro-event-generators
          • Event-macro-proof-preparation
          • Try-event
          • Restore-output?
          • Restore-output
          • Fail-event
          • Cw-event
          • Event-macro-xdoc-constructors
          • Event-macro-intro-macros
        • Def-universal-equiv
        • Def-saved-obligs
        • With-supporters-after
        • Definec
        • Sig
        • Outer-local
        • Data-structures
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Event-macros
    • Make-event

    Make-event-terse

    A variant of make-event with terser screen output.

    We wrap a normal make-event in a with-output that removes all the screen output except possibly errors and except comments. We also suppress the concluding error message of make-event (when an error occurs), via :on-behalf-of :quiet!.

    The :suppress-errors argument determines whether errors should be also suppressed or not. If this argument is nil (the default), errors are not suppressed, but they are not enabled either; that is, they retain the ``status'' they had before. If this argument is non-nil instead, errors are suppressed; make-event-terse will fail silently in case of an error, so errors should not be suppressed in normal circumstances.

    The reason why comments (i.e. the kinds of outputs represented by comment in this list) are not suppressed is that the event macros that use make-event-terse normally support the the :print input, which uses comment output for :result and :info. Thus, these event macro outputs are controlled by :print, and should not be suppressed by make-event-terse.

    We save, via :stack :push, the current status of the outputs, so that, inside the form passed to make-event-terse, the saved output status can be selectively restored for some sub-forms. The saved output status can be restored via (with-output :stack :pop ...), or by using the restore-output or restore-output? utilities.

    Currently make-event-terse does not support make-event's :check-expansion and :expansion?, but it could be extended to support them and pass them to make-event.

    Macro: make-event-terse

    (defmacro
     make-event-terse
     (form &key (suppress-errors 'nil))
     (cons
      'with-output
      (cons
       ':gag-mode
       (cons
        'nil
        (cons
         ':off
         (cons
          (if suppress-errors
              (remove-eq 'comment
                         *valid-output-names*)
              (set-difference-eq *valid-output-names* '(error comment)))
          (cons ':stack
                (cons ':push
                      (cons (cons 'make-event
                                  (cons form '(:on-behalf-of :quiet!)))
                            'nil)))))))))