ACL2-PC::COMM

(macro) display instructions from the current interactive session
Major Section:  PROOF-CHECKER-COMMANDS

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 explained in the documentation for 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 ...) .