|
|
|---|
|
|
|
|---|
An event that always fails with a specified error context, flag, value, and message.
This is realized by always generating a soft error (via er-soft+) during the expansion phase of make-event. The error context, flag, value, and message passed to this macro are not evaluated.
The use of make-event-terse instead of make-event avoids any screen output other than the specified error message.
This macro is used by try-event.
Macro:
(defmacro fail-event (ctx erp val msg) (declare (xargs :guard (msgp msg))) (cons 'make-event-terse (cons (cons 'er-soft+ (cons (cons 'quote (cons ctx 'nil)) (cons (cons 'quote (cons erp 'nil)) (cons (cons 'quote (cons val 'nil)) (cons '"~@0" (cons (cons 'quote (cons msg 'nil)) 'nil)))))) 'nil)))