Custom Query (361 matches)

In case autosending is interrupted but the user hits C-c C-n, automatic sending should be resumed afterwards. (This is suggested in the user manual but not fully working: currently the user needs to modify the buffer first)

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.

[Reported by Michaël Cadilhac]

I'm an Emacs22 user of Proof General, and I experienced some bugs with buffer-invisibility-spec on several occasions.

In GNU Emacs 22.0.93.6 (i686-pc-linux-gnu, X toolkit, Xaw3d scroll bars)
 of 2007-02-09 on mistral
X server distributor `The X.Org Foundation', version 11.0.70101000
configured using `configure  '--prefix=/usr' 'CFLAGS=-O0 -ggdb''

The problem arose when buffer-invisibility-spec was of the form ((smthg . t) t).

Note, I don't know if the patch breaks something with XEmacs. Maybe the following functions aren't defined:

(defun add-to-invisibility-spec (element)
  "Add ELEMENT to `buffer-invisibility-spec'.
See documentation for `buffer-invisibility-spec' for the kind of elements
that can be added."
  (if (eq buffer-invisibility-spec t)
      (setq buffer-invisibility-spec (list t)))
  (setq buffer-invisibility-spec
	(cons element buffer-invisibility-spec)))

(defun remove-from-invisibility-spec (element)
  "Remove ELEMENT from `buffer-invisibility-spec'."
  (if (consp buffer-invisibility-spec)
    (setq buffer-invisibility-spec (delete element buffer-invisibility-spec))))