Next: Manipulating Objects
Up: The Command Language
Previous: The Command Language
The library is a list of the objects defined by the user
and may contain
the theorems, definitions, evaluation bindings and ML code.
Information about the library objects is displayed in the
The jump and scroll commands change what is being
displayed in the library window, while
the move command changes the order of library objects.
The move command is often used to make sure that objects occur before their uses;
this is important for correct library reloading.
- jump object
The library is redisplayed so that the specified entry is visible.
- move objects place
The specified library objects are moved to the position just after the
The library window is moved the specified number of entries, in the
The default direction is down, and the default number of entries is one.
For example, scroll 5 shifts the window down five entries, while
scroll up shifts the window up one entry.
Thu Sep 14 08:45:18 EDT 1995