Ld-prompt
Determines the prompt printed by ld
Ld-prompt is an ld special (see ld). The
accessor is (ld-prompt state) and the updater is (set-ld-prompt val
state). Ld-prompt must be either nil, t, or a function
symbol that, when given an open output character channel and state,
prints the desired prompt to the channel and returns two values: the
number of characters printed and the state. The initial value
of ld-prompt is t.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
However, there are various flags that control ld's behavior and
ld-prompt is one of them. Ld-prompt determines whether ld
prints a prompt before reading the next form from standard-oi.
If ld-prompt is nil, ld prints no prompt. If
ld-prompt is t, the default prompt printer is used, which
displays information that includes the current package, default defun-mode, guard checking status (on or off), and ld-skip-proofsp; see default-print-prompt.
If ld-prompt is neither nil nor t, then it should be a
function name, fn, such that (fn channel state) will print the
desired prompt to channel in state and return (mv col
state), where col is the number of characters output (on the
last line output). You may define your own prompt printing function,
fn, and install it with (set-ld-prompt 'fn state). However, a trust
tag must be active (see defttag) when you set ld-prompt to other
than t or nil (with two exceptions: the functions brr-prompt
and wormhole-prompt, which print the prompt in the break-rewrite
loop and the general wormhole loop, respectively).
If you supply an inappropriate prompt function, i.e., one that
causes an error or does not return the correct number and type of results, the
following odd prompt will be printed instead:
Bad Prompt
See :DOC ld-prompt>
which will lead you to this message. You should either call ld
appropriately next time or assign an appropriate value to
ld-prompt.
