Environment Management Commands

start:

The start command takes a single string argument, a term. A new environment (equation under construction) is started with the term parameter as both left and right side. s is an abbreviation for start.

workback:

The workback command takes a unit argument. This command interchanges the left and right sides of the equation under construction. wb is an abbreviation for workback.

starthere:

The starthere command takes a unit argument and has the effect of the start command called with the right side of the current equation (the term one is looking at) as the parameter.

startover:

The startover command takes a unit argument and has the effect of the start command called with the left side of the current equation (usually the term originally entered; this may be modified by assignment commands and workback) as the parameter.

getenv:

The getenv command takes a single string argument. It retrieves the saved environment named by its argument from the desktop or from the theorem list (if it was saved in a different session). In the latter case position information is lost.

saveenv:

The saveenv command takes a single string argument. It saves the current environment to the desktop and the theorem list, using the argument to name the saved environment. This command causes a theorem display, which was not the case under Mark2.

backupenv:

The backupenv command takes a unit argument. It saves the current environment to the desktop and the theorem list, using the name it already has if it was loaded by the autoedit, getleftside, or getrightside commands, otherwise using the name ``backup''. This command is automatically invoked by some other commands, causing a theorem display which may be unexpected for users of Mark2.

dropenv:

The dropenv command takes a single string argument. It drops the environment named by the argument from the desktop and the theorem list. The backup of the current environment cannot be dropped.

autoedit:

The autoedit command takes a single string argument, the name of a theorem. It creates a new environment with the left side, right side, format and dependencies of the theorem passed to it as an argument. This environment has the name of the theorem.

getleftside, getrightside:

These commands each take a single string argument, the name of a theorem. They have the effect of autoedit called with the same argument followed by startover, starthere respectively.