LP, the Larch Prover -- The history command

The history command produces a list of the commands executed by LP.

Syntax

<history-command> ::= history [ <number> | all ]

Examples

history
history 10
history all

Usage

When supplied with an argument, the history command prints a list of the <number> most recent commands executed by LP or of all commands executed by LP. When not supplied with an argument, it behaves in the same fashion as the last history command (or as history all if it is the first history command).

LP annotates the history by commenting out erroneous commands, by marking the beginning and end of executed files, by marking the creation of subgoals and the completion of proofs, and by indenting the history to reveal its proof structure.

After a thaw command, LP's current history is replaced by the history that led to the corresponding freeze. Thus a script file provides a record of the commands executed during the current LP session, and the history provides a record of commands that will recreate LP's current state.

Users who want a script that will recreate LP's current state, but who have forgotten to issue a set script command, can issue a set log command instead followed by a history all command to capture the script in the log file.