EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Editing Object Reference Terms

Here we explain how to create and modify the various forms of object reference described in doc for ob refs.

Relevant commands: `{obrobref}' `(csm-(mouseright))' `(backspace)' `(c-a)(c-(backspace))' `(mousemiddle)' `(mouseleft)' `show'

BASIC

The basic obref creation command is `{obrobref}', but many other commands will generate obrefs which can then be pasted into your documents.

Applying`{obrobref}' to an empty term slot inserts "[ob name]". You may fill in this text slot however you like, but one special way is this is:

Place the point cursor INSIDE the text slot where the obname is needed, then click `(mousemiddle)' on whatever window you want this obref to point to.

An expeditious way to achieve this is simply to click `(csm-(mouseright))' in whatever object you want to make a pointer to, and it will be inserted.
As usual in this editor, one moves between the various forms of obrefs using the toggling commands `(backspace)' and `(c-a)(c-(backspace))'. doc for toggling.
The short toggle `(backspace)' will cycle through the non-content-displaying methods, or through the content-displaying methods, whereas the long toggle `(c-a)(c-(backspace))' toggles between the content-displaying and non-content-displaying forms.

Let's use the library object sample_of_obref in the examples below.

`(backspace)' starting with sample_of_obref will cycle through these forms:

sample_of_obref The basic form
 
sample_of_obref A slight abbreviation
 
[string] The object name is hidden and the mnemonic string is displayed instead. If you insert the string empty, say by deleting the text then using `(c-d)', it reverts to the sample_of_obref form.

`(c-a)(c-(backspace))' on any of the above forms will "switch tracks" to the following, among which you can toggle with `(backspace)'.
And from these, `(c-a)(c-(backspace))' will switch you back.

Displaying the contents of the object in place:

Sample-Content

Displaying the contents of the object in place, along with the name of the object:

COM Sample-Content

SPECIAL CASES

In an ML editing environment, doc for ML editing, references to theorems of the form "sample_for_thm_obref" will be automatically converted to the form "Thm* 0 = 0" should the point be placed on them. The same goes for references to rule objects.

If the `{obrobref}' command is applied to an instance of a non-system, i.e. a "math" operator, such as "x:. <prop>", then the content-displaying form of a reference to the definiton object will be inserting in it's place: Def x:AB(x) == x:AB(x). The theory motivating this is that one often needs to create pointers to definitions when making documentation, and that the simmplest method is to piggyback on whatever methods one has for getting hold of operator instances in the first place.

About:
intnatural_numberfunctionequalall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

EditorDoc Sections Nuprl Doc