PG

PG copied to clipboard

PG/xml was not putting a newline at the end of the *goals* buffer when there was a single goal. This confused the regexp search in coq-goals--show-first-goal.

Fixes #233 (I think).

@jwiegley could you test whether this PR #342 indeed fixes your reported issue #233 ?

I will test soon, likely tomorrow.

It does solve it, but now PG is very "jumpy". I hit C-c C-RET to get me to the error (this is actually a trick I use to navigate to the next hole, since it's the quickest way to get to exactly where I need to be), and the screen visible flashes, the window shifts the buffer position, then shifts it back, and then finally quiets down and allows me to edit. This will get annoying very quickly when doing it hundreds of times a day...

I guess a principle I'm trying to express is that I'd like PG to continue acting as it does now. If async is enabled, then it's more asynchronous, but it shouldn't feel like a different working environment. The master branch still represents the sort of use experience that I want.

It does solve it, but now PG is very "jumpy".

Hi @jwiegley, which commit did you test ? Because FYI the commit ecd39d515ef6a92c8202d90e27456994dcbb87b4 of this PR wasn't supposed to fix the behavior of C-c C-RET (which has been very improved in #238 AFAICT)

To sum up, do you confirm that the small patch of #342 (proposed by @psteckler just before his leaving) fixes your *goals* issue (regarding the hypotheses that were scrolled out of view)?

OK I just saw your other report #346 (thanks for your feedback!) so I assume you tested the current branch async with patch #342 applied; I'll just wait for your confirmation before merging #342 and closing #233 ;) Erik

Oh, right, I forget about the goals scrolling! I was looking at whether it resets point to the latest error (which it now does).

And yes, I'm testing current master with #342 applied.

@jwiegley thanks for your reply, but just to be sure:

I'm testing current master with #342 applied.

I guess you mean current async with #342 applied, don't you? :) (because the bug #233 solved by this PR didn't impact master AFAIK)

Kind regards, Erik

Should we merge?