Hi, 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. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
