company-coq slows down pasting from system clipboard

[jstolarek]

I use my Emacs in the terminal (no GUI) and often paste some text from the system clipboard into the buffer. (I believe that form Emacs' perspective this is the same as if the text was typed in.) company-coq makes that pasting extremely slow. I measured the time and the pasting speed is around 100 characters per second. The result is that pasting a block of ~80 lines of code takes around half a minute, which is more than annoying. Note that copy-pasting using Emacs' commands (M-w / C-y) works normally, so as a workaround I have to paste text into *scratch* buffer and then M-w/C-y it into Coq buffer.

[cpitclaudel]

Hi,

Thanks for the report. Can you try turning company-mode off? (M-x company-mode). I'd guess this is probably the main factor.

There's no way around the fact that pasting in a terminal is broken, though: as you pointed out, Emacs sees input as series of keypresses, instead of actual characters; this has very annoying side effects, such as \t being seen as a keypress on TAB, for example.

IIRC you compile Emacs yourself. Have you considered using version 25 (the emacs-25 branch of the git repo)? It has support for bracketed paste, which allows terminals to surround paste input with special delimiters, so that Emacs can see it as such. This essentially suppresses the issue.

Clément.

[jstolarek]

Can you try turning company-mode off? (M-x company-mode). I'd guess this is probably the main factor.

Sadly, turning it off does not help :(

as you pointed out, Emacs sees input as series of keypresses, instead of actual characters

Actually, I think I might have been wrong (to some extent at least). For example, say I paste this code:

Example auto_example_1 : ∀(P Q R: Prop), (P → Q) → (Q → R) → P → R.
Proof.
  intros P Q R H1 H2 H3.
  apply H2. apply H1. assumption.
Qed.

Note that ∀ and → are actual unicode characters. They are not supported by Coq so I get a lexer error but only after the whole code (including proof!) has been pasted. If pasting was treated as typing then I should get an error after terminating theorem statement with a dot (electric terminator mode)

Re compiling from git: does the feature you are talking about require special support from the terminal emulator?

[cpitclaudel]

Hmm. It's surprising that turning company-mode off doesn't help. I'll investigate.

Support for bracketed paste is supported in most recent terminal emulator, as far as I know.

[jstolarek]

Let me know if there is any debugging info I can provide.

Support for bracketed paste is supported in most recent terminal emulator

I wonder how recent - I have a distro that is several years old. I guess I'd have to check whether this works for me.