Custom Query (361 matches)

Aquamacs defines various key bindings that are more familiar to Mac users, e.g. cmd-C for copy, cmd-V for paste, etc. These don't work in Proof General. How come?

Isabelle exits in case of erroneous XML input. It could be made more robust, which, e.g., helps debugging in case of editing XML by hand.

One suggestion is to attempt recovery by scanning for the next <pgip opening.

See proof_general_pgip.ML, function loop

To reproduce the bug:

1. Create an empty file one.v, using for example [M-! touch one.v];

2. Create another file two.v with the text

Require Import one.

3. Ensure coq-compile-before-require is true, then script two.v;

the automatic compilation succeeds.

4. Modify one.v, for example by writing something like

Require Export List.

5. Kill buffer *coq-compile-response*, then script again two.v;

the compilation fails with error

condition-case: Selecting deleted buffer

Thanks to the help of the Emacs debugger, I have found the source of the bug:

In function coq-init-compile-response-buffer from coq/coq.el, the first test

(if (bufferp coq-compile-response-buffer)
    …
  …)

is problematic as in this particular state, coq-compile-response-buffer is neither nil nor a relevant buffer value (namely, it is #<killed buffer>, for which bufferp holds).

Moreover, coq-init-compile-response-buffer must beheave well if the user has opened buffer *coq-compile-response* by hand while coq-compile-response-buffer is still nil or #<killed buffer>.

To conclude, I guess we ought to write something like

(if (setq coq-compile-response-buffer
          (get-buffer coq-compile-response-buffer-name))
    …
  …)

to fix both problems.

Kind regards,

Erik Martin-Dorel