saved-errors

(defmacro with-final-error-printing
  (form &key (ctx 'with-final-error-printing))
  `(with-output :off (summary warning!)
    :stack :push (make-event (if (or (f-get-global 'certify-book-info state)
          (global-val 'include-book-path (w state))
          (ld-skip-proofsp state))
        (value '(with-output :stack :pop ,FORM))
        (mv-let (erp val state)
          (with-output :stack :pop (make-event ',FORM))
          (if erp
            (er-progn (assign error-redo-flat-fail
                (f-get-global 'redo-flat-fail state))
              (assign error-redo-flat-succ
                (f-get-global 'redo-flat-succ state))
              (er very-soft
                ',CTX
                "~@0~%"
                (if (boundp-global 'saved-error-for-final-error-printing state)
                  (@ saved-error-for-final-error-printing)
                  "The event failed, but no error message was saved~%"))
              (value '(with-output :off :all (make-event nil))))
            (value `(with-output :off :all (progn (skip-proofs ,(F-GET-GLOBAL 'LAST-MAKE-EVENT-EXPANSION STATE))
                  (value-triple ',VAL))))))))))

(defmacro with-saved-error-msg
  (form msg)
  `(make-event (let ((form ',FORM))
      (er-progn (assign saved-error-for-final-error-printing ,MSG)
        (value `(progn ,FORM
            (with-output :off :all (make-event (let ((state (makunbound-global 'saved-error-for-final-error-printing
                       state)))
                  (value '(value-triple :invisible)))))))))))

(defmacro error-redo-flat
  (&key (succ-ld-skip-proofsp 't)
    (label 'r)
    (succ 't)
    (fail 't)
    (pbt 't)
    (show 'nil))
  `(if (null (f-get-global 'error-redo-flat-fail state))
    (pprogn (fms "
There is no failure saved from a WITH-FINAL-ERROR-PRINTING form.~|"
        nil
        (standard-co state)
        state
        nil)
      (value :invisible))
    ,(IF SHOW
     `(PPROGN
       (FMS "List of events (from encapsulate or progn) preceding ~
                         the failure:~|~%~x0~|"
            (LIST (CONS #\0 (F-GET-GLOBAL 'ERROR-REDO-FLAT-SUCC STATE)))
            (STANDARD-CO STATE) STATE (LD-EVISC-TUPLE STATE))
       (FMS "Failed event:~|~%~x0~|"
            (LIST (CONS #\0 (F-GET-GLOBAL 'ERROR-REDO-FLAT-FAIL STATE)))
            (STANDARD-CO STATE) STATE (LD-EVISC-TUPLE STATE))
       (VALUE :INVISIBLE))
     `(LET ((ERROR-REDO-FLAT-SUCC (F-GET-GLOBAL 'ERROR-REDO-FLAT-SUCC STATE))
            (ERROR-REDO-FLAT-FAIL (F-GET-GLOBAL 'ERROR-REDO-FLAT-FAIL STATE)))
        (STATE-GLOBAL-LET*
         ((ERROR-REDO-FLAT-SUCC ERROR-REDO-FLAT-SUCC)
          (ERROR-REDO-FLAT-FAIL ERROR-REDO-FLAT-FAIL))
         (LD
          (LIST ,@(AND SUCC LABEL `('(DEFLABEL ,LABEL)))
                ,@(AND SUCC
                       (LIST
                        (LIST 'LIST ''LD
                              (LIST 'CONS ''LIST
                                    (LIST 'KWOTE-LST 'ERROR-REDO-FLAT-SUCC))
                              :LD-SKIP-PROOFSP SUCC-LD-SKIP-PROOFSP)))
                ,@(AND FAIL
                       (LIST
                        (LIST 'LIST ''LD
                              (LIST 'LIST ''LIST
                                    (LIST 'LIST ''QUOTE 'ERROR-REDO-FLAT-FAIL))
                              :LD-ERROR-ACTION :CONTINUE :LD-PRE-EVAL-PRINT
                              T)))
                ,@(AND PBT SUCC LABEL
                       `('(PPROGN (NEWLINE (PROOFS-CO STATE) STATE)
                                  (PBT ',LABEL)))))))))))

(defmacro saved-error-cond
  (&rest conds)
  `(with-output :off :all (make-event (cond . ,(SAVED-ERROR-COND-FN CONDS)))))

(defmacro skip-proofs-outside-certify
  (form)
  (skip-proofs-outside-certify-fn form))