Event-macro-results
Results of event macros.
Many event macros generate events in the ACL2 world.
Some event macros may also generate files,
e.g. macros that generate code in other programming languages from ACL2.
We refer to these generated events, and possibly files,
as results of the event macro.
This nomenclature is particular relevant to
the screen printing performed by the event macros:
see event-macro-screen-printing.
When the :print input is :result or higher,
generated events are normally printed on screen as Lisp forms.
However, in some cases only their names and short descriptions are printed
(e.g. when they are large and thus not necessarily useful
to see in their entirety every time,
or when they have a regular predictable structure);
in these cases, the Lisp forms can be seen, if desired,
by querying the ACL2 world (e.g. with pe).
When an event macro generates files
and :print is :result or higher,
the file paths are normally printed, but not the file contents,
which can be seen by opening the files.
