Observation
Print an observation
Here is a typical application of observation.
ACL2 !>(let ((ctx 'top-level)
(name 'foo))
(observation ctx
"Skipping processing of name ~x0."
name))
ACL2 Observation in TOP-LEVEL: Skipping processing of name FOO.
<state>
ACL2 !>
Observation prints an initial ``ACL2 Observation...: '', and then
prints the indicated message using formatted printing (see fmt).
Notice in the example above that evaluation of a call of observation
returns state. Indeed, observation is actually a macro whose
expansion takes and returns the ACL2 state. A similar utility,
observation-cw, is available that does not take or return state;
rather, it returns nil as the suffix ``cw'' suggests that a
``comment window'' is the target of this printing, rather than the state. For
example:
ACL2 !>(let ((ctx 'top-level)
(name 'foo))
(observation-cw ctx
"Skipping processing of name ~x0."
name))
ACL2 Observation in TOP-LEVEL: Skipping processing of name FOO.
NIL
ACL2 !>
Observation-cw takes exactly the same arguments as observation,
but observation-cw does its printing in a so-called ``wormhole''; see
wormhole.
General Forms:
(observation ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
(observation-cw ctx fmt-string fmt-arg1 fmt-arg2 ... fmt-argk)
where ctx generally evaluates to a symbol (but see below), and
fmt-string together with the fmt-argi are suitable for passing to
fmt. Output begins and ends with a newline.
Recall from the example above that the output from a call of
observation (or observation-cw) begins with ``ACL2
Observation'' and additional characters ending in ``: '', for example
`` in TOP-LEVEL: '', followed by formatted output produced from
fmt-string with the given fmt-argi. The characters printed
immediately following the string ``ACL2 Observation'' depend on the value
of ctx. If ctx is nil, nothing is printed. If ctx is a
non-nil symbol, it is printed using fmt directive ~x. If
ctx is a cons pair whose car is a symbol, formatted
printing is applied to the string "(~x0 ~x1 ...)", where #\0 and
#\1 are bound respectively to that car and cdr. Otherwise, ctx is
printed using fmt directive ~@.
We next discuss situations in which printing is inhibited for
observation and observation-cw. No printing is done when
observation is among the inhibited output types; see set-inhibit-output-lst. Moreover, no printing is done by observation
during include-book. If you want to avoid printing from
observation-cw during include-book, then you need to manage that
yourself.
