Stefan Monnier monn...@iro.umontreal.ca writes:
I think this deserves an Emacs bug report.
see http://debbugs.gnu.org/cgi/bugreport.cgi?bug=13400
There are definitely some documentation problems.
process-send-string is not mentioned as function that might
trigger a filter call.
I think
I wrote:
here is a patch that solves the problem for me. Any comments?
I committed now. I deleted the argument of proof-shell-filter, to
make sure, nobody will use it. Reasons are described in the doc
comments.
Hendrik
___
ProofGeneral-devel
Hello Hendrik
Quick thoughts: this sounds like a pretty fundamental problem and
surprising if we hadn't come across it before. Do you definitely see
this in the ordinary running code, not just when using the debugger?
Maybe prooftree input is different case to prover input.
If we need to