Custom Query (361 matches)

Hello,

I have just noticed the ProofGeneral function proof-undo-and-delete-last-successful-command does not really meet the specification that is described in its documentation, namely:

... the deleted command is put into the Emacs kill ring, so
you can use the usual `yank' and similar commands to retrieve the
deleted text.

I have performed a few tests and it seems sufficient to replace

(proof-undo-last-successful-command-1 'delete-region)

with

(proof-undo-last-successful-command-1 'kill-region)

in generic/pg-user.el to provide the missing feature.

Kind regards,

Erik Martin-Dorel

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*>

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.