Jason Gross

> Do you think it would be better to block the UI while typing, rather than right after processing a definition? No. Can you set it up to block the...

> Can you set it up to block the UI only when the user hasn't given emacs any keyboard input Note that something like this might already be implemented for...

> But it's a bit tricky to get right: I need to find a time when it's safe to send input to Coqtop, and that's not trivial. How about this?...

How does inline-docs (`M-f12`?) work without breaking everything, then?

@cpitclaudel *poke* This is still way too slow. I'm hitting cases where it takes > 9 seconds to fetch symbol data. Somehow, when I do `M-x company-coq-toggle-definition-overlay`, company Coq gives...

I believe my usage pattern is strongly clustered around a very short delay between commands, with a long tail. If 90% of the time that I edit a file within...

> if we detect a keystroke or something like that while fetching completions, we cancel the whole process and return control to you immediately Sounds good! (Assuming that emacs doesn't...

Thanks, will do On Tue, Oct 10, 2017, 5:53 AM Clément Pit-Claudel wrote: > Ok, I think I can look at this next week, when I come back to the...

Here are some backtraces: 1. ``` Debugger entered--Lisp error: (quit) redisplay_internal\ \(C\ function\)() ``` 2. ``` company-coq: Loading symbols… Error running timer `company-coq-maybe-reload-each': (error "Proof General: quit in proof-shell-wait") Quit...

In a file close to the end, but not at the end of the pipeline: ``` Time Add Search Blacklist "Raw" "Proofs". (* Finished transaction in 0. secs (0.u,0.s) (successful)...