LP, the Larch Prover -- The set prompt command


The prompt setting defines a string that LP uses to prompt users to enter a command.

Syntax

<set-prompt-command> ::= set prompt <prompt> 
<prompt>             ::= <blank-free-string> | ` <string> '

Examples

set prompt `[!] '
set prompt `>> '

Usage

By default, <prompt> is `LP!: ', which causes LP to issue prompts of the form "LP1: ", "LP2: ", ... To enter a prompt that begins or ends with a space, enclose it within `' marks.

LP replaces the first exclamation mark (!) in <prompt>, if any, by the number of the next command. LP numbers commands entered from the terminal by consecutive integers. It numbers commands obtained during execution of a script (.lp) file by appending a period followed by consecutive integers to the number of the execute command; thus command 5.2.3 is the third command in the script file executed in response to the second command in the script file executed in response to the fifth command typed by the user.