LD-PROMPT

determines the prompt printed by 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.