Opened 10 years ago

Closed 10 years ago

Last modified 10 years ago

#372 closed defect (invalid)

funny => sign all over my scripts

Reported by: megacz Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:


for some reason proof general 4.0 is putting this funny "=>" symbol all over my scripts. What's going on?

Attachments (2)

pg-bug2.v (85 bytes) - added by megacz 10 years ago.
Screen shot 2010-10-07 at 11.44.55 PM.png (44.3 KB) - added by megacz 10 years ago.

Download all attachments as: .zip

Change History (6)

comment:1 Changed 10 years ago by megacz

To reproduce: download the attachment. Type:

emacs -nw pg-bug2.v

Twiddle your fingers while basking in the glorious glow of the proof general splash screen.

Type "C-c ." to turn on electric terminator.

Move to the end of the file. Delete the existing period and re-type it.

Move the cursor up two lines.

Type "M-x" and "proof-retract-until-point-interactive".

You'll see what's in the attached screenshot. The script has become illegible. This is not good.

Changed 10 years ago by megacz

Attachment: pg-bug2.v added

Changed 10 years ago by megacz

comment:2 Changed 10 years ago by David Aspinall

Resolution: invalid
Status: newclosed

This is the "overlay arrow", you are seeing the crude tty equivalent of a nice arrow that appears in the Emacs margin for GUI Emacsen. It points to the next position to be processed by the prover. (It's used in the Emacs debugger similarly).

It seems not too bad if most of your script lines are indented by two or more spaces but otherwise would be a bit annoying, for sure. To disable it you can put a line in your =.emacs= file:

   (setq overlay-arrow-string nil)

or, less crudely, just for proof scripts:

(add-hook 'proof-mode-hook
          (lambda () (set (make-local-variable 'overlay-arrow-string) nil)))

You could instead change it to be a one character string if that is less invasive.

(Is there any reason to stick to tty Emacs for PG these days?)

comment:3 Changed 10 years ago by megacz

Thanks, any chance that the default could be changed to match PG3.7? This seems like a nice feature, but enabling it by default is a confusing behavior change.

Regarding tty emacs, I look at it from the other direction: I don't use the mouse (many reasons, including RSI), so non-tty emacs has nothing to offer me -- especially now that I can get unicode fonts and colors in the terminal. I also think that Apple's is better at displaying grids of characters than the Free Software Foundation's oft-neglected GUI code. And I have ssh-only access to some very, very fast machines.

comment:4 Changed 10 years ago by David Aspinall

Understand your reasons for tty use, although support is secondary for PG as you're probably in a small minority. Agree with you about behaviour changes being confusing but I will leave as is, since it is a general Emacs feature applied in a fairly obvious way for PG. Wouldn't want to backport/hide use of other Emacs features as they evolve. People should expect changes in 4.0 version bump.

Note: See TracTickets for help on using tickets.