next up previous contents index
Next: Manipulating Objects Up: The Command Language Previous: The Command Language

Library Display

  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 library  window. 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 specified place.

  The library window is moved the specified number of entries, in the specified direction. 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.

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995