*response* buffer only showing last output

[andremoeller]

*response* buffer only showing last output

[Matafou]

Hi,

You have 2 configurable options:

• proof-keep-response-history which, if t, allow to navigate back and forth in the history of responses
• proof-tidy-response which, if non t, clean up the response buffer less often.
  C-h v <name of the variable> for a few more precision.
  If this fits your need, please close this issue.
  Best regards,

[Matafou]

Ho and you also have another feature that can be useful:

• M-x proof-store-goals-win (C-c C-a g) : stores (cumulatively) the current of the goals buffer into a special buffer
• proof-store-response-win (C-c C-a r): same thing with response buffer.
  These can be useful if you want to keep some goal or answer visible while scripting around.

[andremoeller]

Perfect -- thank you so much! Closing this issue as answered.