EditorDoc Sections Nuprl Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Executing ML code with `(c-z)'. doc for ml execution cmds

If the point is within a term whose operator is marked with the ml_string condition, such as:

DO <ml>

DO <ml>

ML> <ml command>
<term>

APPLY> <ml fn>
<term>

jump to the smallest one containing the point, else stay where you are, then:

1. If it's ML> <ml command> <term>
then execute the command leaving the answer in a certain space provided for it.
 
2. If it's APPLY> <ml fn> <term>
then replace the covered term by the result of applying the ML function to it.
 
3. Else, if you're in a Goal or Rule box for a THM, then check it with the possible effect on the subproofs.
 
4. Else, evaluate the term in ML and leave the textual answer on the stack.

It is easy to open up a command area wherever you are by inserting the cover

ML> <ml command>
<term>

with `ml(return)' and it easy to remove the cover with `(c-d)'. IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
EditorDoc Sections Nuprl Doc