try-event

(in-package "ACL2")

(define try-event
  (form ctx erp val (msg msgp))
  :returns (event pseudo-event-formp)
  :parents (event-macros)
  :short "Try to submit an event,
          generating a customized error if the submission fails."
  :long (topstring (p "This is useful to “replace” the error generated by an event
     (e.g. a @(tsee defun) or a @(tsee defthm))
     with a customized soft error.
     The event is submitted with all output off (including error output),
     so there is no output if the submission succeeds.
     If the submission fails,
     @(tsee orelse) is used to submit a @(tsee fail-event) to cause an error
     with the specified context, flag, value, and message."))
  `(orelse (with-output :gag-mode nil :off :all ,FORM)
    (fail-event ,CTX ,ERP ,VAL ,MSG)))