Custom Query (361 matches)

Newlines in PGIP console (e.g. in parseresult) are lost.

Hopefully these can be recovered from the document parse and are lost somewhere else.

[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))))

Dear Proof General Developers,

When Coq issues a warning inside a proof, PG shows the warning in the minibuffer, but it does not show the resulting goal.

For example:

Goal True /\ True -> True.
intro H.
destruct H as [H1 H2 H3].

After the last command, the minibuffer contains "[Coq] Warning: Unused introduction pattern : H3", but the *response* buffer is empty. The same happens if I process

Require Import Setoid.
Goal False.
setoid_replace False with True.

The minibuffer contains a truncated warning "[Coq] Warning: There are several relations of the carrier 'Prop'. The relation (P", but the response buffer is again empty.

I am not sure what the correct behavior in this case should be (should PG display the warning *and* the goal?), but the goal should probably be displayed.

I am using CVS snapshot of PG updated on September 3, 2007 and Coq trunk 10056.

Thank you, Evgeny