Opened 14 years ago

Last modified 10 years ago

#377 reopened defect

Electric-terminator mode next line movement changed

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

Description

When electric-terminator mode is enabled, after I type a period the cursor immediately moves to the leftmost position on the following line. This is a behavior change from PG3.7 and quite annoying.

Change History (8)

comment:1 Changed 14 years ago by David Aspinall

Milestone: PG-Emacs-4.0 → PG-Emacs-4.1
Status: new → accepted

Yes, this was supposed to be part of configurable behaviour for advancing point but got hard-wired, apologies. Here's a quick hack to prevent: 

  (defun proof-script-next-commmand-advance ())

comment:2 Changed 14 years ago by megacz

Putting those lines in my .emacs file does not fix the problem. Help!

comment:3 Changed 13 years ago by David Aspinall

Sorry, I missed seeing your plea until now!

You need to overwrite that function after PG is loaded, something like: 

 (eval-after-load "proof-script"
   '(defun proof-script-next-commmand-advance ())
  )

should do it. Note quote before defun.

comment:4 Changed 13 years ago by David Aspinall

Milestone: PG-Emacs-4.1 → PG-Emacs-4.2

comment:5 Changed 12 years ago by David Aspinall

Resolution: → fixed
Status: accepted → closed

User option proof-next-command-insert-space added which can be used to turn this behaviour off.

comment:6 Changed 10 years ago by coquser

Milestone: PG-Emacs-4.2 → PG-Emacs-4.3
Resolution: fixed
Status: closed → reopened
Summary: cursor moves to the next line after I type a period → Electric-terminator mode next line movement changed

Reopening this ticket as I'm having the same issue (and as #433), using the latest development release ProofGeneral-4.3pre131011.

I'm new to Coq and am completing the Software Foundations textbook, so I'm inserting proofs into pre-existing files. It'd be great to have electric-mode to facilitate playing about quickly, but the line movement issue is causing me big problems. I've attempted to follow the steps above, but the configuration option isn't taking effect.

I'm new to ProofGeneral, Emacs and Lisp, but I think I've traced the source of the error:

Although the function proof-script-new-command-advance does indeed use the new option proof-next-command-insert-space, the electric terminator doesn't actually appear to use this function.

proof-assert-electric-terminator calls proof-script-next-command-advance, rather than proof-script-new-command-advance.

Last edited 10 years ago by coquser (previous) (diff)

comment:7 Changed 10 years ago by coquser

I can confirm this (version 4.3~pre130510-1.1). The fix in comment:3 doesn’t work either.

Last edited 10 years ago by coquser (previous) (diff)

comment:8 Changed 10 years ago by coquser

Patched noted in comment:6 has been applied to my personal tree at ​https://github.com/edgemaster/ProofGeneral-patches/commit/25d3dca8f7f2858d59ce46fd4c604d1b6c62194e

Works well enough for me.

Note: See TracTickets for help on using tickets.