Custom Query (361 matches)

Step 1: In a theory file buffer, type a character like "-" or ".", which is an initial character in a Unicode shortcut sequence. The character displays with an underline, indicating this.

Step 2: Press "delete", intending to delete the chararacter to the right of the insertion point.

Result: The character that I just typed ("-" or ".") is deleted instead, as if I had pressed "backspace".

C-h k shows that "delete" is bound to unicode-tokens-delete-char, and "backspace" is bound to unicode-tokens-delete-backward-char. It appears that while entering a unicode token shortcut (when characters are shown with the underline) both of these do the same thing.

Versions: Isabelle Proof General, Version 4.1pre101216; GNU Emacs 23.2.1 (i686-pc-linux-gnu, GTK+ Version 2.21.6); Isabelle 2011; Ubuntu 10.10.

To reproduce the bug:

1) have in file foo.v the following:

Eval compute in 0.

2) Have in file bar.v the following:

Require Import foo.

3) then try to script bar.v (with auto-compilation on), compilation of foo.v is started automatically but then there is an error due to the read-only status of coq-compile-response buffer. I think this is due to the fact that coqc compilation *does* the output.

Cheers, P.

excerpt of buffer *Messages*:

Check /home/courtieu/titi.vo Recompile /home/courtieu/titi.v Waiting for process to die...done condition-case: Buffer is read-only: #<buffer *coq-compile-response*>

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