ACL2-pc::comm
(macro)
display instructions from the current interactive session
Examples:
comm
(comm 10)
General Form:
(comm &optional n)
Prints out instructions in reverse order. This is actually the same as
(commands n t) — or, (commands nil t) if n is not
supplied. As for commands (see ACL2-pc::commands), the final
argument of t causes suppression of instructions occurring between
so-called ``matching bookends,'' which we now explain.
A ``begin bookend'' is an instruction of the form
(COMMENT :BEGIN x . y).
Similarly, an ``end bookend'' is an instruction of the form
(COMMENT :END x' . y').
The ``name'' of the first bookend is x and the ``name'' of the second
bookend is x'. When such a pair of instructions occurs in the current
state-stack, we call them ``matching bookends'' provided that they have the
same name (i.e. x equals x') and if no other begin or end bookend
with name x occurs between them. The idea now is that comm hides
matching bookends together with the instructions they enclose. Here is a more
precise explanation of this ``hiding''; probably there is no value in reading
on!
A comm instruction hides bookends in the following manner. (So does a
comment instruction when its second optional argument is supplied and
non-nil.) First, if the first argument n is supplied and not
nil, then we consider only the last n instructions from the
state-stack; otherwise, we consider them all. Now the resulting list of
instructions is replaced by the result of applying the following process to
each pair of matching bookends: the pair is removed, together with everything
in between the begin and end bookend of the pair, and all this is replaced by
the ``instruction''
("***HIDING***" :COMMENT :BEGIN name ...)
where (comment begin name ...) is the begin bookend of the pair.
Finally, after applying this process to each pair of matching bookends, each
begin bookend of the form (comment begin name ...) that remains is
replaced by
("***UNFINISHED***" :COMMENT :BEGIN name ...) .
