hendriktews
hendriktews
> how do you handle commands like all: split in prooftree? This is not working. Prooftree assumes that all new subgoals are children of the last current goal. > all:...
Thanks for your contribution! In #514 I described an approach that sets and clears the timer for each command sent to Coq. Instead, your approach is to set and clear...
> It seems to work, but is it really what we expect? No. It seems that my comment from March 21, that the approach followed here is also possible, was...
Instead of filtering proof-assistant-settings for empty commands, I would suggest to not add `coq-diffs` to proof-assistant-settings for Coq < 8.10.
I believe the problem comes from coq-mode not being defined in coq.el - this was introduced by @monnier in f7cc8f1f76baf5e517e51f1db47510ed605064e8. Other assistants rely on the stub that is created from...
It's not working with what you can find on github. Sorry about this. I'll reply here with instructions after I uploaded what I have on disk.
See #468 for measuring the difference between silent and non-silent processing.
@Matafou @cpitclaudel Do you have an opinion here? Shall we make delayed response/goal processing more complicated or simply switch to non-silent?
@Matafou: Maybe my goals are not so long. In one of the tested files I see about 1400 goals printed, maximum size 88 lines, average 41, and about 700 goals...
The approach of this PR is to submit a Show command after the error to update the goals buffer while keeping the error message somehow visible. A completely different approach...