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

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to