David Aspinall <david.aspin...@ed.ac.uk> writes: At a quick glance this looks like a reasonable way to fix without messing with the current filter code. Luckily, I don't think the str argument is used.
I'm not completely clear on the error case, is the idea just to give up if we hit an error in some call? If proof-shell-filter signals an error, the error is just propagated, only the active flag is reset to enable later calls again. Or do you mean the case where a parallel, overlapping call is detected? In this case the -was-blocked flag is set and the already running instance of the wrapper stays for one more iteration in the while loop, thus calling proof-shell-filter after the previous call finished. This effectively delays Coq until prooftree catches up. This is just what you want, I believe. Under normal circumstances prooftree is much faster than Coq. Because of the experience with PVS, where the proof tree visualizer was often the bottleneck, I made some special optimizations: - tree layout is linear in the tree depth; for PVS it is apparently worse than linear in the number of nodes - tree display is delayed until no display commands are available on input; nevertheless, when asserting large regions, you see the tree growing node by node, indicating that prooftree is faster than Coq Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
