SET-SAVED-OUTPUT

save proof output for later display with :pso or :pso!
Major Section:  OTHER

Examples:
(set-saved-output t t)    ; save proof output for later, but inhibit it now
(set-saved-output :all t) ; same as the line above
:set-saved-output t t     ; same as the two lines above
(set-saved-output t nil)  ; save proof output for later, but print it now too
(set-saved-output nil t)  ; do not save proof output, and print it now
(set-saved-output nil nil); do not save or inhibit output
(set-saved-output nil :normal)  ; default: do not save output, and only
                                ; inhibit proof-tree output 

General Form: (set-saved-output save-flg inhibit-flg)

Parameter save-flg is t or :all to cause output to be saved for later display using pso or pso!; see pso and see pso!, and see the documentation for proof-checker commands of the same names. Set save-flg to nil to turn off this feature; except, it always stays on in proof-checker sessions entered with verify. The other argument, inhibit-flg, controls whether output should be inhibited when it is created (normally, during a proof attempt). So a common combination is to set both arguments to t, to indicate that output should be suppressed for now but saved for printing with pso or pso!. The examples above give a good summary of the functionality, including the meaning of values :all and :normal for the first and second arguments (respectively).

Saved output is cleared at the start of every event, and also at the start of every proof-checker commands that invoke the prover. Note that interactive proof-checker commands, that is, from a proof-checker session entered with verify, are always run with output saved.

Also see set-print-clause-ids, which causes subgoal numbers to be printed during proof attempts when output is inhibited.