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
ProofGeneral-devel@inf.ed.ac.uk
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.

Reply via email to