The relevant editor commands are shown in
Table 
Table: Commands For Changing and Closing Windows
Term editor window are opened by using the ML view command on a library object. They are also opened by the proof editor, when then proof editor SELECTSELECT command is issued on sequents and ruleboxes, and when the proof editor TRANSFORMTRANSFORM command is given.
EXIT first saves a copy of the object. It then checks the object before closing the window. This checking has the same effect on library objects as using the ML check command.
If the check fails, then the window is left open. If
you still want to close the
window, use QUITQUIT. Seperate save and check commands are
described in Section
.
QUIT is an abort command. It closes the window, abandoning any changes made to the window since it was last checked by attempting EXIT.
JUMP-NEXT-WINDOW allows one to cycle around all the currently open windows, including any proof editor windows.
JUMP-ML moves the cursor over to the ML top-loop window.