ld
Major Section: MISCELLANEOUS
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.
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.
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.
