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
proof-shell-handle-error-or-interrupt, however:

- 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

Reply via email to