Electric terminator and newlines

[proofgeneral]

Electric terminator and newlines

[jstolarek]

(setq coq-one-command-per-line nil does the job! Thanks.

[Matafou]

Hi,
I also see the problem when the option Coq One Command Per Line is enable
too, is it the case for you? If this option is disable then the cursor
stays after the dot.

Do you think that if Coq One Command Per Line is enable we should always
insert a newline? Wouldn't it be annoying too to have to remove that
newline from time to time?

P.

Le mar. 16 févr. 2016 à 16:15, Ondřej Slámečka [email protected] a
écrit :

Hello,

I am using the electric terminator mode and I have "Proof Next Command
Insert Space" enabled but when I enter a terminator ('.' in coq) PG moves
the cursor ('|' in the example below) to the next line, where I usually
have 'Qed.' so I have to do C-p after writing a line in my proof. Is this
an expected behaviour or a bug?

    exact a.

| Qed.

I am using GNU Emacs 24.5.1, ProofGeneral (downloaded today from GitHub),
company-coq and the following minor modes.

Auto-Composition Auto-Compression Auto-Encryption
Blink-Cursor Company Company-Coq Company-Coq--Keybindings
Diff-Auto-Refine Electric-Indent File-Name-Shadow Font-Lock
Global-Font-Lock Holes Hs Line-Number Menu-Bar Mouse-Wheel Outline
Prettify-Symbols Proof-Active-Buffer-Fake
Proof-Electric-Terminator-Enable Show-Paren Tooltip Transient-Mark Yas

—
Reply to this email directly or view it on GitHub
#53.

[OndrejSlamecka]

Yes, the problem appears when Coq One Command Per Line is enabled.
In my experience the cases when newline insertion (unless the proof is finished) would benefit me are far more common than those when I would have to delete the newly created line.

[jstolarek]

I believe I am facing the same problem. If I am editing at the end of file (ie. the mark is followed by EOF) then inserting a terminator (ie. a dot) does not move to the next line. This is expected. But if I go back in my proof script and start editing somewhere in the middle of a file then inserting terminator moves the cursor to the next line. What I would expect is that the cursor remains in the same line just as it does when I edit my proof at the end of file. Current behaviour is extremely annoying and forces me to manually go back to previous line after inserting a dot. It is almost impossible to work in such a setting so I usually comment out the rest of the file, cut the proof I am editing, move it to the end of the file and once it is finished move it back to its original location and uncomment the rest of the file. This happens with Coq 8.5 and ProofGeneral from the repo (dbfe0a4). Here are my PG settings from .emacs file:

(setq proof-splash-enable nil)
(setq proof-colour-locked nil)
(setq proof-electric-terminator-enable t)
(setq proof-three-window-mode-policy 'hybrid)

[Matafou]

OK I will (soon) make it add a newline instead of going down one line.

Meanwhile you can set coq-one-command-per-line to nil.

P.

2016-04-12 11:24 GMT+02:00 Jan Stolarek [email protected]:

I believe I am facing the same problem. If I am editing at the end of file
(ie. the mark is followed by EOF) then inserting a terminator (ie. a dot)
does not move to the next line. This is expected. But I go back in my proof
script and start editing somewhere in the middle of a file then inserting
terminator moves the cursor to the next line. What I would expect is that
the cursor remains in the same line just as it does when I edit my proof at
the end of file. Current behaviour is extremely annoying and forces me to
manually go back to previous line after inserting a dot. It is almost
impossible to work in such a setting so what I usually comment out the rest
of the file, cut the proof I am editing, move it to the end of the file and
once it is finished move it back to its original location and uncomment the
rest of the file. This happens with Coq 8.5 and ProofGeneral from the repo (
dbfe0a4
dbfe0a4).
Here are my PG settings from .emacs file:

(setq proof-splash-enable nil)
(setq proof-colour-locked nil)
(setq proof-electric-terminator-enable t)
(setq proof-three-window-mode-policy 'hybrid)

—
You are receiving this because you commented.
Reply to this email directly or view it on GitHub
#53 (comment)