Manipulating Objects

These are the commands that directly manipulate  objects. The most used of these commands is view, since most interaction with the system takes place within the editors started up by the view command.

archive objects

  For each object name specified a copy of the object is made and saved as the old version of the object. The library window is redisplayed if any of the archived objects are visible in the window. Note that there is no way to delete, modify or unarchive an object.

check objects

   Each of the indicated objects is checked. Checking an object makes the objects defined therein available for use in other objects. When an object is checked, its status is updated, as is the status of any object that references any of the specified objects. If necessary the library window is redisplayed to show the new statuses.

Checking a large theorem can take awhile. If the body of the theorem was dumped to a file and has not been fully reloaded (see the dump and load commands below) then checking the theorem brings in and reconstructs the body of the proof.

create name kind place

  A new library entry of the specified name and kind is created at the specified place. The library is redisplayed so that the newly created object is the first object in the library window. The object will be empty and its status will be RAW.

delete objects

  The specified objects are removed from the library. The status of any entry depending on these objects is set to BAD. (This status change has been fully implemented only for definition objects.)

view object

  The object is displayed in a new window. If old is specified the archived version of the object will be viewed and the view will be read--only; otherwise, the unarchived version of the object will be viewed. If the object is not already being viewed the new view will be fully editable; otherwise, it and all other views of the object will be made read--only. The header line of the view will say SHOW for a read--only view and EDIT for an editable view.

The editor used depends on the kind of object. The refinement editor ( red) is used on theorems, while the text  editor ( ted) is used for other objects. For more information on ted and red see sections 7.4 and 7.5, respectively. Typing in an edit window will make delete the window and end its editing of the object. If there are other edit views on the screen the cursor will be placed in one of them; otherwise, the cursor will go back to the command window.

When view is done on a large theorem, it may take some time to activate red. If the body of the theorem has been dumped but not fully reloaded (see the dump and load commands below) then reads the body in and reconstructs it before starting the editor.