I would like to properly display errors that occur when
recompiling coq modules.
In my current patch error reporting is broken.
It seems the error reporting function is
- Does proof-shell-handle-error-or-interrupt work as expected,
when called from inside proof-extend-queue?
- proof-shell-handle-error-or-interrupt copies the error message
from proof-shell-last-output into the response buffer. In my
case the error message comes from (call-process "coqc" ...). I
can either let call-process write directly into the response
buffer or use some other buffer. Copying the error message into
proof-shell-last-output seems not to be the right way.
How to report those coqc errors? I believe I need a
refactorization of proof-shell-handle-error-or-interrupt where I
can pass the error message as a string argument.
ProofGeneral-devel mailing list