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.
Looking at what you've done so far, I suggest simply not sending the
commands to the theorem prover process if the auto compilation fails.
Your own error reporting brings up a helpful buffer which shows the
result of the coqc command, and adjusting the proof-shell patch as below
prevents the queue being left in a bad state.
- D.
*** generic/proof-shell.el 10 Oct 2010 22:57:05 -0000 11.0
--- generic/proof-shell.el 12 Jan 2011 13:17:27 -0000
***************
*** 924,932 ****
--- 924,938 ----
for processing a region from (buffer-queue-or-locked-end) to END.
The queue mode is set to 'advancing"
(proof-set-queue-endpoints (proof-unprocessed-begin) end)
+ (condition-case err
+ (run-hooks 'proof-shell-extend-queue-hook)
+ (error
+ (proof-detach-queue)
+ (signal (car err) (cdr err))))
(proof-add-to-queue queueitems 'advancing))
_______________________________________________
ProofGeneral-devel mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
