Missing test in proof-store-buffer-win

[Erik Martin-Dorel]

If I run proof-store-goals-win or proof-store-response-win while the Coq process is not loaded, the low-level error

let: Wrong type argument: stringp, nil

occurs in proof-store-buffer-win, since there is no *goals* nor *response* buffer.

We should probably add a test in proof-store-buffer-win that raises a more friendly error if ever the buffer argument is nil.

Kind regards, Erik Martin-Dorel

[David Aspinall]

Thanks for the report. Considering this further:

I hadn't noticed these functions, I wonder about replacing/generalising them.

The standard clone-buffer didn't work because of mode functions clearing the buffer by default --- I've fixed that now, so perhaps we can base these functions on that after all. The default behaviour of clone-buffer is not to pop up a new frame, however; although this would happen in multiple frame mode, and it might be handy if the bindings work in single frame/terminal mode too.

There is other experimental code lying around to keep a history in the response/goals buffer themselves (keys to browse back and forth), but functions in coq.el provide something different, a convenient copy to a notepad.

Let's ask Pierre about it.

[David Aspinall]

Pierre likes the current function behaviour so we'll keep it, despite feature proliferation...

[Erik Martin-Dorel]

Thank you for your comments.

I have a related remark:

In the Emacs info page [C-h i g (emacs)Non-Window Terminals], I saw that Emacs can also handle multiple frames in a text-only terminal. Thus the current frame popup behavior seems to be tty-compliant.