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>