EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
`dfadj' kbd_dfadjust

(apply) If current_object is a conventionally named display ob corresponding to an active ABS object, then imitate the display forms of term t for the operator of the ABS object. The parm types and arity much match modulo permuation.

When the whole disp object is empty, or it is a standard display spec with an empty place for the model:

Converts variables to display templates and converts op-parms to display-meta-parms if they are slots, abstraction-meta-parms, or level-expressions. If the term is an obref to a verified abstraction object, then the definiendum (lhs) is used instead. Also, if the term is a placeholder and the current object name ends with `_df`, then it's as if it were an obref using the same name with the `_df` chopped off. DO Review cmds for group: "DisplaySpec"

Also add a menu of display children derived from the display meta-vars.

Otherwise, treating the term filling the DISP object as a sample, try to imitate the display methods that are used for the term filling the object by looking up its display forms, and looking up the term defined by the ABS object corresponding to the new display object.
For this to work, there must be an active ABS object whose name is derived form the new DISP object by removing _df from the end, and the sample term must have the same parm types and arity as the definiendum of the ABS object, modulo permuation.

See `adj'. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc