Nuprl - doc for ob refs

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Object Reference Terms, or obrefs.

This editor recognizes a special class of terms as references to objects, which expand in ML code to the token naming the object, and on which `(mouseleft)' or `show' will cause the referenced object to be viewed.

An obref always contains a pointer to the object, but there are three basic display methods (plus some combinations).
Here we discuss the variously displaying forms of object reference terms; we'll discuss their creation and editing in doc for ob refs editing.

For this explanation, we have created a sample comment object sample_of_obref containing the following: Sample-Content.

1. The first way of displaying an object reference is to indicate the name of the object, and possibly a hint that it is an object reference. The default form ordinarily inserted via the `{obrobref}' is exemplified above, namely: sample_of_obref. A trivial variation is sample_of_obref.

2. The second form is to simply stipulate the text to be displayed such as THIS, possibly with some hint that it is an obref.

3. The third is to show the content of the object, again exemplified above, though not obviously so, namely: Sample-Content.
There are some variations on this content display form.
One is to show both content and name, thus:
COM Sample-Content

When a content-displaying form is used on an object other than a comment object, the kind of object is indicated as well. When such a form is used to display a theorem, `(mouseleft)' will expose the theorem content in a browsable form rather than raising the proof.
Example: Thm* 0 = 0
The "*" indicates that the proof is good and complete.
Clicking `(mouseleft)' on this theorem obref will convert the form which merely shows the content, to one containing the content for perusal or cut-n-paste editing.
Clicking `(mouseleft)' again on the "Thm:" notation will restore the obref.
(Further, to enhance readability, it is not necessarily the exact content that is displayed with these indirect content-displaying forms of obref, but rather, it is the result of applying the function ob_content_display_adjust to the object name.)

doc for ob refs editing for how to edit obrefs.

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc

1.	The first way of displaying an object reference is to indicate the name of the object, and possibly a hint that it is an object reference. The default form ordinarily inserted via the `{obrobref}' is exemplified above, namely: sample_of_obref. A trivial variation is sample_of_obref.

2.	The second form is to simply stipulate the text to be displayed such as THIS, possibly with some hint that it is an obref.

3.	The third is to show the content of the object, again exemplified above, though not obviously so, namely: Sample-Content. There are some variations on this content display form. One is to show both content and name, thus: COM Sample-Content When a content-displaying form is used on an object other than a comment object, the kind of object is indicated as well. When such a form is used to display a theorem, `(mouseleft)' will expose the theorem content in a browsable form rather than raising the proof. Example: Thm* 0 = 0 The "*" indicates that the proof is good and complete. Clicking `(mouseleft)' on this theorem obref will convert the form which merely shows the content, to one containing the content for perusal or cut-n-paste editing. Clicking `(mouseleft)' again on the "Thm:" notation will restore the obref. (Further, to enhance readability, it is not necessarily the exact content that is displayed with these indirect content-displaying forms of obref, but rather, it is the result of applying the function ob_content_display_adjust to the object name.)