EXECUTE-FILE : MEXPREXECUTE-FILE is a top-level command.
Execute commands from a SAVE-WORK file.
Call this from the main top level or the proofwindows top level of TPS.
Note that this will not save subsequent commands in the same file,
which distinguishes it from RESTORE-WORK.
In the cases where EXECUTE-FILE doesn't work, one can usually just
load the .work file into an editor and then cut and paste it, whole,
into the TPS window.
Single-stepping only works between commands on the main top level;
it will not stop at prompts which are internal to a command, nor between
commands on a different top level. To force a work-file to stop in
such a place, use the PAUSE command when creating the work file.
If you are single-stepping through a file, you can
abort at any time by typing ^G<RETURN>.
The command format for EXECUTE-FILE is:
<n>EXECUTE-FILE COMFIL EXECPRINT OUTFIL STEPPING
"FILESPEC" "YESNO" "FILESPEC" "YESNO"
The arguments have the following meaning:
COMFIL : SAVE-WORK file
EXECPRINT : Execute Print-Commands?
OUTFIL : Output file ("NUL:" to discard)
STEPPING : Single Step Operation?
TPS documentation homepage