Custom Query (361 matches)

Hi,

the commit ​http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/ProofGeneral/rev/d3cf65e2d4e4 brakes parsing in Coq. Try

Require Export Coq.Lists.List.
Notation "[ ]" := nil : list_scope.
Notation "[ a ; .. ; b ]" := (a :: .. (b :: []) ..) : list_scope.

Bye,

Hendrik

In Emacs23.3, when replacing tokens like \<Longrightarrow>, they are not recognized as wide characters, i.e. emacs thinks, they are still as wide as a normal character. This leads to problems, as emacs then overprints parts of the inserted character.

It does work when inserting the unicode symbol itself (i.e. not using the token-support) - so it does not look like an emacs problem per se.

Even more interesting, it also works flawlessly with emacs 23.2.

This was tested with ProofGeneral-4.1pre101216-p1 and ProofGeneral-4.1pre110601

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