Desktop

A desktop consists of several workspaces on the desktop and one current workspace. The workspaces on the desktop may include a version of the current workspace. Each workspace is associated with a theory (there can be no more than one workspace associated with each theory); the name of a workspace (unless it is ``scratch'') will be the name of a saved theory file.

The new commands versiondate and script are treated as desktop commands more or less by default, as are some recently introduced commands for controlling behavoir of scripts.

Desktop commands include

versiondate:

Displays the date of the version of Mark2 being used.

script <string>:

This command has the effect of the ML use command, but adds the extension .mk2 to its argument. Files with this extension are to be expected to be ML proof scripts. The script command no longer uses the ML interpreter; a new file parser has been writtem.

setpause, setnopause:

setpause causes the prover to pause whenever it issues an error message. This is useful when running proof scripts. setnopause reverses this effect.

bequiet, speakup:

bequiet suppresses all output usually seen from proof scripts, except error messages. speakup reverses this effect, which is necessary if normal prover function is to be restored.

noml:

Invokes a new interface which uses the same file parser as the script command. Commands in this interface have the same format as in the ML interface, as long as the new file parser is familiar with the command. The () (type unit) parameter to commands which don't have a real parameter is optional with this interface; the null quit command exits this interface (and must end scripts to be run by the script command).

demoline <string>:

Used to make comments with pauses in demo scripts.

initializecounter:

Sets the new variable counter to zero. Useful in scripts, as otherwise names of new variables prove unpredictable.

storeall <string>:

Save the current workspace to a theory file whose name is the argument with an extension added (currently ``.wthy'').

safesave:

Stores the current workspace to a file; determines the argument from the name of the workspace.

load <string>:

Load a saved theory from the theory file indicated by the argument, backing up the current theory onto the desktop.

clear:

Set the current theory to ``scratch'' (nothing but the logic prelude).

clearpredicative:

As clear, with the additional ``predicativity'' restrictions on abstraction. Of technical interest only.

gettheory <string>:

The argument is the name of a theory. Get this theory off the desktop (backing up the current theory unless the name of the current theory itself is the argument).

backuptheory:

Save the current theory on the desktop.

exportthm, exportthmlist (parameters not indicated):

Commands for theorem export. Parameters of exportthmlist are a view name, a prefix to add to constants automatically generated, a prefix to add to operators automatically generated, a list of theorems to be exported, and the name of the target theory (which must be on the desktop). Parameters of exportthm omit the prefix for operators and replace the list of theorems with a single theorem. Theorem export is likely to generate many warnings of repeated constant declarations.