		Search-engine friendly clone of the ACL2 documentation.

Event-macros

Event-macro-screen-printing

Screen printing performed by event macros.

Event macros normally print messages on the screen when they run. At a minimum, they should print error messages, e.g. when user inputs do not pass validation. Event macros are run to produce results, namely events and sometimes files, which should be typically printed on the screen to confirm that the event macro has done its job, and also to inform the user of some details of the results. Sometimes it is useful to have event macros print additional information as they run, about their internal operation, e.g. to help debug when they do not seem to behave as expected. Furthermore, a user may sometimes want to see the complete output produced by ACL2 in response to the events produced by an event macro, not just the external (i.e. exported) events, but also the internal (i.e. local) events. In certain cases, a user may want to suppress all screen output, including any error messages.

The above discussion suggests five ordered levels of screen printing, specified by the :print input of the event macros that adhere to this convention, i.e. the event macros whose user documentation references this manual page. The ordered printing levels, which are the possible values of the :print input, are

nil < :error < :result < :info < :all

where the amount of printed material increases monotonically.

When :print is nil, nothing is printed (not even errors).

When :print is :error, only errors (if any) are printed.

When :print is :result, besides errors (if any), also the results of the event macro are printed, as described in the manual page just referenced.

When :print is :info, besides errors (if any) and results, also some additional information about the event macro's operation is printed.

When :print is :all, besides errors (if any), results, and additional information, also all the ACL2 output in response to the submitted events is printed