Broken Keybindings for Show Me -> ... and others

[Generic Isabelle user]

Using Proof General 4.0pre100709, 4.0pre100815 or 3.7.11 and Gnu Emacs 23.1.1 (in Debian), all key bindings in the Isabelle -> Show Me -> ... menu (and a few others) are broken.

They are displayed by emacs as e.g. "C-c C-a <h> <c>" which does not seem to be a valid key binding. Expected would be e.g. "C-c C-a C-h C-c".

This seems to be due to wrong use/definition of proof-definvisible:

(proof-definvisible isar-help-cases "print_cases" [h c])

yields a broken binding, but

(proof-definvisible isar-cmd-quickcheck "quickcheck" [(control q)])

a working one.

[David Aspinall]

Fixed, many thanks for reporting. I think the bindings used an XEmacs syntax. NB: the bindings are "C-c C-a h c" etc.

[Generic Isabelle user]

Thank you for the quick fix!

I would suggest changing the key binding for refute to C-c C-a C-r instead of C-c C-a r to be consistent with Quickcheck, Nitpick et al.