Major Section: IO
Each of ACL2's formatted printing functions,
FM*, has an analoguous macro
FM*-TO-STRING indicated below. These functions do not include a channel
state as an argument, and
FM*-TO-STRING returns the string that
FM* would print to the state, in place of
state; see fmt. The legal
keyword arguments are described below.
General Forms: result (fms-to-string string alist &key ...) ; string (fmt-to-string string alist &key ...) ; (mv col string) (fmt1-to-string string alist column &key ...) ; (mv col string) (fms!-to-string string alist &key ...) ; string (fmt!-to-string string alist &key ...) ; (mv col string) (fmt1!-to-string string alist column &key ...) ; (mv col string)
The legal keyword arguments are as follows. They are all optional with a
Evisc-tupleis evaluated, and corresponds exactly to the
evisc-tupleargument of the corresponding
FM*function; see fmt.
Fmt-control-alistshould typically evaluate to an alist that maps print-control variables to values; see print-control. Any alist mapping variables to values is legal, however. By default the print controls are set according to the value of constant
fmt-control-alistoverrides these defaults.
tis also a legal value. See set-iprint for the effect of value
t, which however is local to this call of a
FM*-TO-STRINGfunction; the behavior if iprinting afterwards is not affected by this call. In particular, you will not be able to look at the values of iprint tokens printed by this call, so the value
tis probably of limited utility at best.
Also see io for a discussion of the utility
which allows for accumulating the results of more than one printing call into
a single string but requires the use of