Pierre Courtieu

I can make legacy/pg issue a Show after each (group of) commands, actually I alrady do that in some cases. It could be triggered with >8.7 versions. P. 2017-06-01 19:11...

I just pushed a fix for this on PG side: When the user backtracks inside a proof, pg issues a "Unset Silent. Show.". when the backtrack is done outside a...

Yes it would be nice. Again for efficiency reason on big goals I would rather not send Show blindly all the time. Ideally, at least in xml/protocol Show should return...

Experience will tell. By the way is there a priority system in the protocol? Like "stop this heavy computation of a part of the file I am not currently looking...

PG sets/unsets silent when scripting several commands at a time. This avoids the heavy useless outputs from coq (which emacs then reads) when scripting big chunks of files. This problem...

You can probably just script back one line and and then forward to make things appear again. Le lun. 13 nov. 2017 à 23:05, benzrf a écrit : > Alright....

Coming back to this. I already fixed a few cases where the goal would not show up by inserting a "Show." command. But there is still an annoying case where...

Thanks @hendriktews. I will try that. But the problem is that it is during the treatment of an error message that we detect that we should send a "Show" to...

Here you go: https://github.com/ProofGeneral/PG/pull/429 P. Le ven. 12 juil. 2019 à 19:59, hendriktews a écrit : > Pierre Courtieu writes: > > > I managed to put the action in...

Hi. Bad news :-(. @erikmd, do you think we can add the special build of the melpa package as a test in our CI?