I have some code running that recompiles coq modules if
necessary just before the require command is sent to coqtop. I
came across two problems:

1. The recompilation is done inside a callback called
   asynchronously from proof-shell-invoke-callback. There are
   various reasons why the compilation could fail. In such a case
   I have to flush proof-action-list and signal an error to the
   user. In my first attempt I used

     (error "Some error message..." ... )

   which does not work.

   How should I signal an error from inside the callback?

   Shall I write the error message into *response* and invoke
   proof-shell-handle-error-or-interrupt? However, my error
   messages coming from coqdep or coqc and not from coqtop.

2. Items in the proof-action-list have the form


   Could someone elaborate on the form of COMMANDS? Why is it a
   list (and not just a string)? Are there cases where this list
   contains something else than just one string?


ProofGeneral-devel mailing list

Reply via email to