Adding New Terms

The insertion commands  for terms are shown in Table . These commands are only appropriate with a term cursor.

  
Table: Term Insertion

name in these commands is a string of characters, naming a new term to be inserted. The interpreter for name strings checks each of the following conditions until it finds one which applies.

1. name  is an editor command enabled in a particular context. See sections for examples.

2. name is an alias  for some display form, defined in in the library object for that display form.

3. name is the name of a display form object. It refers to the first display form defined in that object.

4. name is of the form ni where n is the name of a display form object and i is a natural number. ni refers to the ith display form definition in the object named n. Definitions in objects are numbered starting from 1.

5. name is the name of an abstraction object, then name refers to the earliest display form in the library for that abstraction.

6. name is allnumerals  , then the term referred to is the natural-number name:n () term of Nuprl's object language.

7. name refers to the variable term variable name:v ().

Names always have acceptable extensions as variable names, so the editor doesn't interpret name until some explicit terminator is typed. For example, this can either be NO-OP ( SPACE ) or a cursor motion command. NEXT-EMPTY-SLOT (C- RETURN ) is a particularly useful terminator.

INSERT-TERM- NAME is only applicable at empty term slots. It results in the display form referred to by name being inserted into the slot. If name is terminated by a NO-OP, then a term cursor is left at the new term. If name is teminated by some cursor motion command, then that command is obeyed.

INSERT-TERM-LEFT NAME is intended for use at a filled term slot. Its behavior is to:

1. save  the existing term in the slot, leaving the slot empty,
2. insert  the new display form referred to by name into the slot,
3. paste  the saved term into the left-most term slot of the new display form. If the new display form has no term slots, then the saved term is lost.

INSERT-TERM-RIGHT NAME behaves in a similar way to INSERT-TERM-LEFT except that in step 3, the saved term is pasted into the right-most term slot of the new display form.

SUBSTITUTE-TERM- NAME allows you to replace one display form with another which has the same sequence of child text and term slots. The children of the old display form become the children of the new display form. In the event that the new display form has a different sequence of children SUBSTITUTE-TERM- NAME tries something vaguely sensible. In general, in these cases, it is safer to explicitly cut and paste the children.

INITIALIZE-TERM initializes a term slot to some default term if one is appropriate. The term slot must initially be empty. INITIALIZE-TERM is automatically invoked by Nuprl to initialize new windows. If you want to re-initialize a window, place a term cursor at the root of the term in the window, delete the term, and then give the INITIALIZE-TERM command. The default terms for particular contexts are described in various sections of this document. If no default has been designated, INITIALIZE-TERM does nothing.

SELECT-DFORM-OPTION when the term cursor is at certain terms, selects an alternative display  form for that term. For example, if term cursor is positioned at an independent function type, it selects the more general dependent-function display form.