Custom Query (361 matches)

GNU Emacs 23.1.1, Mac OS.

The point movement after asserting commands is still a bit odd. With proof-assert-next-command there is a higher change that it moves after the span than with proof-goto-point, where it seems to move to the span start unconditionally. But there are situations where both fail.

Also note that proof-goto-point does not work if the point is at the first position of the command keyword.

currently, when hitting backspace after a Unicode symbol, the symbol is changed into its ascii form. This means that it takes 13 backspaces to remove a \<Rightarrow>. It would be nice if delete removes the whole symbol - I rarely edit the ascii body of symbols I've typed. Mostly I want to remove them and type something else. If we want to keep the current editing mode, maybe make it an option in PG menus.

Hello,

In the past, when PG was started, Emacs showed the splash screen with PG portrait for a few seconds and then switched to the proof script buffer that I was going to edit. The splash screen occupied the whole Emacs frame.

For many months now, during startup the frame is split in two vertically. The bottom buffer has the splash screen, while the top part briefly shows the *Messages* buffer and then switches to the script file. The frame stays split with the splash buffer at the bottom. This happens in particular with .emacs file having only one line that loads PG. (See my Emacs version below.)

I prefer the earlier behavior. Currently, the big version of the PG portrait I got from the EPS file does not fit the bottom half frame :-(

Emacs : GNU Emacs 23.1.50.1 (i486-pc-linux-gnu, GTK+ Version 2.12.9)

of 2009-08-01 on radon, modified by Debian

Package: Proof General

current state: ============== (setq

proof-general-version "Proof General Version 4.0pre100709. Released by da." proof-assistant "Coq" )

Evgeny