Hi,
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
(SPAN COMMANDS ACTION [DISPLAYFLAGS])
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?
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
