Many commands automatically display the current term and the selected subterm. One can use the look command to do this at any time, or the lookhere command to see just the selected term. The lookback command allows one to view the left side of the equation.
The display of terms uses a scheme of indentation meant to suggest the precedence structure of the term. This can be fine-tuned in various ways. The setline command will set line length. The setdepth command will set a limit on how deep into the parse tree subterms will be displayed; the nodepth command removes such a limit.
The precedence of operators can be reset at any time using the setprecedence command.
The current dependency list (axioms and definitions used in the proof so far) can be seen using seedeps.