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 ...) .
