Major Section: MISCELLANEOUS
Examples:
:max ; the command most recently typed by the user
:x ; synonymous with :max
(:x -1) ; the command before the most recent one
(:x -2) ; the command before that
:x-2 ; synonymous with (:x -2)
5 ; the fifth command typed by the user
1 ; the first command typed by the user
0 ; the last command of the system initialization
-1 ; the next-to-last initialization command
:min ; the first command of the initialization
:start ; the last command of the initial ACL2 logical world
fn ; the command that introduced the logical name fn
(:search (defmacro foo-bar))
; the first command encountered in a search from :max to
; 0 that either contains defmacro and foo-bar in the
; command form or contains defmacro and foo-bar in some
; event within its block.
The recorded history of your interactions with the top-level ACL2 command loop is marked by the commands you typed that changed the logical world. Each such command generated one or more events, since the only way for you to change the logical world is to execute an event function. See command and see events. We divide history into ``command blocks,'' grouping together each world changing command and its events. A ``command descriptor'' is an object that can be used to describe a particular command in the history of the ongoing session.
Each command is assigned a unique integer called its ``command number'' which indicates the command's position in the chronological ordering of all of the commands ever executed in this session (including those executed to initialize the system). We assign the number 1 to the first command you type to ACL2. We assign 2 to the second and so on. The non-positive integers are assigned to ``prehistoric'' commands, i.e., the commands used to initialize the ACL2 system: 0 is the last command of the initialization, -1 is the one before that, etc.
The legal command descriptors are described below. We use n to
denote any integer, sym to denote any logical name
(see logical-name), and cd to denote, recursively, any command
descriptor.
command command
descriptor described
:max -- the most recently executed command (i.e., the one with
the largest command number)
:x -- synonymous with :max
:x-k -- synonymous with (:x -k), if k is an integer and k>0
:min -- the earliest command (i.e., the one with the smallest
command number and hence the first command of the system
initialization)
:start -- the last command when ACL2 starts up
n -- command number n (If n is not in the
range :min<=n<=:max, n is replaced by the nearest of :min
and :max.)
sym -- the command that introduced the logical name sym
(cd n) -- the command whose number is n plus the command number of
the command described by cd
(:search pat cd1 cd2)
In this command descriptor, pat must be either an atom or
a true list of atoms and cd1 and cd2 must be command
descriptors. We search the interval from cd1 through cd2
for the first command that matches pat. Note that if cd1
occurs chronologically after cd2, the search is
``backwards'' through history while if cd1 occurs
chronologically before cd2, the search is ``forwards''. A
backwards search will find the most recent match; a
forward search will find the chronologically earliest
match. A command matches pat if either the command form
itself or one of the events in the block contains pat (or
all of the atoms in pat if pat is a list).
(:search pat)
the command found by (:search pat :max 0), i.e., the most
recent command matching pat that was part of the user's
session, not part of the system initialization.
