- goals should be reset when there are no more goals (does work)
- goals should be reset after Qed (does not work)

Extend the goals present tests to additionally check that the response
buffer contains some text (i.e., an error message) in those cases
where an error is expected.

- After Search and Check the goals should be up-to-date and the
  response should be visible, also in two-pane mode.
- Extend existing tests to check that the response is also visible in
  two-pane mode, if applicable.
- Use Proof General variables containing the buffer instead of buffer
  names.