display instructions from the current interactive session
Major Section: PROOF-CHECKER-COMMANDS
Examples: comm (comm 10)Prints out instructions in reverse order. This is actually the same as
General Form: (comm &optional n)
(commands n t)-- or,
(commands nil t)if
nis not supplied. As explained in the documentation for
commands, the final argument of
tcauses 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
xand 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') and if no other begin or end bookend with name
xoccurs between them. The idea now is that
commhides 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!
comm instruction hides bookends in the following manner. (So does
comment instruction when its second optional argument is supplied
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 ...) .