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 outputParameter
General Form: (set-saved-output save-flg inhibit-flg)
:allto cause output to be saved for later display using
pso!; see pso and see pso!, and see the documentation for proof-checker commands of the same names. Set
nilto 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!. The examples above give a good summary of the functionality, including the meaning of values
:normalfor 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.